# HG changeset patch
# User wenzelm
# Date 1252103737 -7200
# Node ID cc5d388fcbf26274311f36f63ff8f59deb035de3
# Parent  cce1dcc923dc42137694853134756946c5a3b871
eliminated MarkupInfo, moved particular variants into object Command;

diff -r cce1dcc923dc -r cc5d388fcbf2 src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Sat Sep 05 00:15:14 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Sat Sep 05 00:35:37 2009 +0200
@@ -17,7 +17,7 @@
 import org.gjt.sp.jedit.Buffer
 import org.gjt.sp.jedit.TextUtilities
 
-import isabelle.prover.RefInfo
+import isabelle.prover.Command
 
 
 class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
@@ -62,9 +62,9 @@
           val line = buffer.getLineOfOffset(begin)
           val end = theory_view.to_current(document, command_start + ref.stop)
           ref.info match {
-            case RefInfo(Some(ref_file), Some(ref_line), _, _) =>
+            case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
               new ExternalHyperlink(begin, end, line, ref_file, ref_line)
-            case RefInfo(_, _, Some(id), Some(offset)) =>
+            case Command.RefInfo(_, _, Some(id), Some(offset)) =>
               prover.get.command(id) match {
                 case Some(ref_cmd) =>
                   new InternalHyperlink(begin, end, line,
diff -r cce1dcc923dc -r cc5d388fcbf2 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Sat Sep 05 00:15:14 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Sat Sep 05 00:35:37 2009 +0200
@@ -43,6 +43,14 @@
     val FINISHED = Value("FINISHED")
     val FAILED = Value("FAILED")
   }
+
+  case object RootInfo
+  case class HighlightInfo(highlight: String) { override def toString = highlight }
+  case class TypeInfo(type_kind: String) { override def toString = type_kind }
+  case class RefInfo(file: Option[String], line: Option[Int],
+    command_id: Option[String], offset: Option[Int]) {
+      override def toString = (file, line, command_id, offset).toString
+    }
 }
 
 
@@ -79,9 +87,9 @@
 
   lazy val empty_root_node =
     new MarkupNode(0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
-      Nil, content, RootInfo())
+      Nil, content, Command.RootInfo)
 
-  def markup_node(begin: Int, end: Int, info: MarkupInfo): MarkupNode =
+  def markup_node(begin: Int, end: Int, info: Any): MarkupNode =
   {
     val start = symbol_index.decode(begin)
     val stop = symbol_index.decode(end)
diff -r cce1dcc923dc -r cc5d388fcbf2 src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Sat Sep 05 00:15:14 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Sat Sep 05 00:35:37 2009 +0200
@@ -12,21 +12,9 @@
 import isabelle.proofdocument.ProofDocument
 
 
-abstract class MarkupInfo
-case class RootInfo() extends MarkupInfo
-case class HighlightInfo(highlight: String) extends
-  MarkupInfo { override def toString = highlight }
-case class TypeInfo(type_kind: String) extends
-  MarkupInfo { override def toString = type_kind }
-case class RefInfo(file: Option[String], line: Option[Int],
-  command_id: Option[String], offset: Option[Int]) extends MarkupInfo {
-    override def toString = (file, line, command_id, offset).toString
-  }
-
-
 class MarkupNode(val start: Int, val stop: Int,
   val children: List[MarkupNode],
-  val content: String, val info: MarkupInfo)
+  val content: String, val info: Any)
 {
 
   def swing_tree(make_node: MarkupNode => DefaultMutableTreeNode): DefaultMutableTreeNode =
diff -r cce1dcc923dc -r cc5d388fcbf2 src/Tools/jEdit/src/prover/State.scala
--- a/src/Tools/jEdit/src/prover/State.scala	Sat Sep 05 00:15:14 2009 +0200
+++ b/src/Tools/jEdit/src/prover/State.scala	Sat Sep 05 00:35:37 2009 +0200
@@ -36,28 +36,28 @@
   lazy val highlight_node: MarkupNode =
   {
     markup_root.filter(_.info match {
-      case RootInfo() | HighlightInfo(_) => true
+      case Command.RootInfo | Command.HighlightInfo(_) => true
       case _ => false
     }).head
   }
 
   lazy private val types =
     markup_root.filter(_.info match {
-      case TypeInfo(_) => true
+      case Command.TypeInfo(_) => true
       case _ => false }).flatten(_.flatten)
 
   def type_at(pos: Int): String =
   {
     types.find(t => t.start <= pos && t.stop > pos).map(t =>
       t.content + ": " + (t.info match {
-        case TypeInfo(i) => i
+        case Command.TypeInfo(i) => i
         case _ => "" })).
       getOrElse(null)
   }
 
   lazy private val refs =
     markup_root.filter(_.info match {
-      case RefInfo(_, _, _, _) => true
+      case Command.RefInfo(_, _, _, _) => true
       case _ => false }).flatten(_.flatten)
 
   def ref_at(pos: Int): Option[MarkupNode] =
@@ -92,14 +92,15 @@
                 if (begin.isDefined && end.isDefined) {
                   if (kind == Markup.ML_TYPING) {
                     val info = body.first.asInstanceOf[XML.Text].content
-                    st.add_markup(command.markup_node(begin.get - 1, end.get - 1, TypeInfo(info)))
+                    st.add_markup(
+                      command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
                   }
                   else if (kind == Markup.ML_REF) {
                     body match {
                       case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
                         st.add_markup(command.markup_node(
                           begin.get - 1, end.get - 1,
-                          RefInfo(
+                          Command.RefInfo(
                             Position.file_of(attr),
                             Position.line_of(attr),
                             Position.id_of(attr),
@@ -108,7 +109,8 @@
                     }
                   }
                   else {
-                    st.add_markup(command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind)))
+                    st.add_markup(
+                      command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
                   }
                 }
                 else st