changeset 281:26fbdf02e4e5

unify header newlines
author Markus Kaiser <markus.kaiser@in.tum.de>
date Sun, 23 Sep 2012 19:21:25 +0200
parents e2a93acfa936
children 71419d49716d
files src/isabelle/LocaleBrowser/graph_xml.scala src/isabelle/LocaleBrowser/layout_pendulum.scala src/isabelle/LocaleBrowser/model.scala src/isabelle/LocaleBrowser/mutator.scala src/isabelle/LocaleBrowser/popups.scala src/isabelle/LocaleBrowser/tooltips.scala src/isabelle/LocaleBrowser/visualizer.scala
diffstat 7 files changed, 12 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/src/isabelle/LocaleBrowser/graph_xml.scala	Sun Sep 23 19:18:32 2012 +0200
+++ b/src/isabelle/LocaleBrowser/graph_xml.scala	Sun Sep 23 19:21:25 2012 +0200
@@ -9,6 +9,7 @@
 
 import isabelle._
 
+
 case class Locale(val axioms: List[XML.Body], val parameters: List[(String, XML.Body)])
 
 object Graph_XML
--- a/src/isabelle/LocaleBrowser/layout_pendulum.scala	Sun Sep 23 19:18:32 2012 +0200
+++ b/src/isabelle/LocaleBrowser/layout_pendulum.scala	Sun Sep 23 19:21:25 2012 +0200
@@ -9,6 +9,7 @@
 
 import isabelle._
 
+
 object Layout_Pendulum {
   type Key = String
   type Entry = Option[Locale]
--- a/src/isabelle/LocaleBrowser/model.scala	Sun Sep 23 19:18:32 2012 +0200
+++ b/src/isabelle/LocaleBrowser/model.scala	Sun Sep 23 19:21:25 2012 +0200
@@ -4,8 +4,8 @@
 Internal graph representation.
 */
 
+package isabelle.graphview
 
-package isabelle.graphview
 
 import isabelle._
 import isabelle.graphview.Mutators._
@@ -13,6 +13,7 @@
 import scala.actors.Actor
 import scala.actors.Actor._
 
+
 class Mutator_Container(val available: List[Mutator[String, Option[Locale]]]) {
     type Mutator_Markup = (Boolean, Color, Mutator[String, Option[Locale]])
     
--- a/src/isabelle/LocaleBrowser/mutator.scala	Sun Sep 23 19:18:32 2012 +0200
+++ b/src/isabelle/LocaleBrowser/mutator.scala	Sun Sep 23 19:21:25 2012 +0200
@@ -10,6 +10,7 @@
 import java.awt.Color
 import scala.collection.immutable.SortedSet
 
+
 trait Mutator[Key, Entry]
 {
   val name: String
--- a/src/isabelle/LocaleBrowser/popups.scala	Sun Sep 23 19:18:32 2012 +0200
+++ b/src/isabelle/LocaleBrowser/popups.scala	Sun Sep 23 19:21:25 2012 +0200
@@ -15,6 +15,7 @@
 import scala.swing.MenuItem
 import scala.swing.Separator
 
+
 object Popups {
   def apply(panel: Graph_Panel, under_mouse: Option[String],
             selected: List[String]): JPopupMenu =
@@ -29,7 +30,7 @@
             def apply =
               add_mutator(
                 Mutators.create(
-                  Vertex_List(ls, reverse, false, false)
+                  Node_List(ls, reverse, false, false)
                 )
               )
           })
@@ -38,7 +39,7 @@
             def apply =
               add_mutator(
                 Mutators.create(
-                  Vertex_List(ls, reverse, true, true)
+                  Node_List(ls, reverse, true, true)
                 )
               )
           })
@@ -47,7 +48,7 @@
             def apply =
               add_mutator(
                 Mutators.create(
-                  Vertex_List(ls, reverse, false, true)
+                  Node_List(ls, reverse, false, true)
                 )
               )
           })
@@ -56,7 +57,7 @@
             def apply =
               add_mutator(
                 Mutators.create(
-                  Vertex_List(ls, reverse, true, false)
+                  Node_List(ls, reverse, true, false)
                 )
               )
           })
--- a/src/isabelle/LocaleBrowser/tooltips.scala	Sun Sep 23 19:18:32 2012 +0200
+++ b/src/isabelle/LocaleBrowser/tooltips.scala	Sun Sep 23 19:21:25 2012 +0200
@@ -10,6 +10,7 @@
 import isabelle._
 import java.awt.FontMetrics
 
+
 object Tooltips {
   // taken (and modified slightly) from html_panel.scala
   private def make_HTML(term: XML.Body, fm: FontMetrics): String = {
--- a/src/isabelle/LocaleBrowser/visualizer.scala	Sun Sep 23 19:18:32 2012 +0200
+++ b/src/isabelle/LocaleBrowser/visualizer.scala	Sun Sep 23 19:21:25 2012 +0200
@@ -10,6 +10,7 @@
 import java.awt.RenderingHints
 import java.awt.Graphics2D
 
+
 class Visualizer(val model: Model) {
   object Coordinates {
     private var nodes = Map[String, (Double, Double)]()