prefer statically typed Text.Markup;
authorwenzelm
Fri Nov 11 14:24:38 2011 +0100 (2011-11-11 ago)
changeset 454554f974c0c5c2f
parent 45454 388fb71623dd
child 45456 9ba615ac75fb
prefer statically typed Text.Markup;
src/Pure/PIDE/blob.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/text.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
     1.1 --- a/src/Pure/PIDE/blob.scala	Fri Nov 11 14:07:20 2011 +0100
     1.2 +++ b/src/Pure/PIDE/blob.scala	Fri Nov 11 14:24:38 2011 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  {
     1.5    sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
     1.6    {
     1.7 -    def + (info: Text.Info[Any]): State = copy(markup = markup + info)
     1.8 +    def + (info: Text.Markup): State = copy(markup = markup + info)
     1.9    }
    1.10  }
    1.11  
     2.1 --- a/src/Pure/PIDE/command.scala	Fri Nov 11 14:07:20 2011 +0100
     2.2 +++ b/src/Pure/PIDE/command.scala	Fri Nov 11 14:24:38 2011 +0100
     2.3 @@ -25,12 +25,12 @@
     2.4      /* content */
     2.5  
     2.6      def add_status(st: Markup): State = copy(status = st :: status)
     2.7 -    def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
     2.8 +    def add_markup(m: Text.Markup): State = copy(markup = markup + m)
     2.9      def add_result(serial: Long, result: XML.Tree): State =
    2.10        copy(results = results + (serial -> result))
    2.11  
    2.12 -    def root_info: Text.Info[Any] =
    2.13 -      new Text.Info(command.range,
    2.14 +    def root_info: Text.Markup =
    2.15 +      Text.Info(command.range,
    2.16          XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
    2.17      def root_markup: Markup_Tree = markup + root_info
    2.18  
    2.19 @@ -53,7 +53,7 @@
    2.20                if id == command.id && command.range.contains(command.decode(raw_range)) =>
    2.21                  val range = command.decode(raw_range)
    2.22                  val props = Position.purge(atts)
    2.23 -                val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
    2.24 +                val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    2.25                  state.add_markup(info)
    2.26                case _ =>
    2.27                  // FIXME System.err.println("Ignored report message: " + msg)
     3.1 --- a/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 14:07:20 2011 +0100
     3.2 +++ b/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 14:24:38 2011 +0100
     3.3 @@ -19,7 +19,7 @@
     3.4  
     3.5    object Branches
     3.6    {
     3.7 -    type Entry = (Text.Info[Any], Markup_Tree)
     3.8 +    type Entry = (Text.Markup, Markup_Tree)
     3.9      type T = SortedMap[Text.Range, Entry]
    3.10  
    3.11      val empty = SortedMap.empty[Text.Range, Entry](Text.Range.Ordering)
    3.12 @@ -41,7 +41,7 @@
    3.13  
    3.14    val empty = new Markup_Tree(Branches.empty)
    3.15  
    3.16 -  type Select[A] = PartialFunction[Text.Info[Any], A]
    3.17 +  type Select[A] = PartialFunction[Text.Markup, A]
    3.18  }
    3.19  
    3.20  
    3.21 @@ -55,7 +55,7 @@
    3.22        case list => list.mkString("Tree(", ",", ")")
    3.23      }
    3.24  
    3.25 -  def + (new_info: Text.Info[Any]): Markup_Tree =
    3.26 +  def + (new_info: Text.Markup): Markup_Tree =
    3.27    {
    3.28      val new_range = new_info.range
    3.29      branches.get(new_range) match {
    3.30 @@ -126,7 +126,7 @@
    3.31    }
    3.32  
    3.33    def swing_tree(parent: DefaultMutableTreeNode)
    3.34 -    (swing_node: Text.Info[Any] => DefaultMutableTreeNode)
    3.35 +    (swing_node: Text.Markup => DefaultMutableTreeNode)
    3.36    {
    3.37      for ((_, (info, subtree)) <- branches) {
    3.38        val current = swing_node(info)
     4.1 --- a/src/Pure/PIDE/text.scala	Fri Nov 11 14:07:20 2011 +0100
     4.2 +++ b/src/Pure/PIDE/text.scala	Fri Nov 11 14:24:38 2011 +0100
     4.3 @@ -115,6 +115,8 @@
     4.4        catch { case ERROR(_) => None }
     4.5    }
     4.6  
     4.7 +  type Markup = Info[XML.Tree]
     4.8 +
     4.9  
    4.10    /* editing */
    4.11  
     5.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Nov 11 14:07:20 2011 +0100
     5.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Nov 11 14:24:38 2011 +0100
     5.3 @@ -152,7 +152,7 @@
     5.4      val root = data.root
     5.5      val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     5.6      for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
     5.7 -      snapshot.command_state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
     5.8 +      snapshot.command_state(command).root_markup.swing_tree(root)((info: Text.Markup) =>
     5.9            {
    5.10              val range = info.range + command_start
    5.11              val content = command.source(info.range).replace('\n', ' ')