merged, resolving minor conflicts;
authorwenzelm
Mon, 02 Mar 2009 19:27:06 +0100
changeset 34534 b06946a1d4cb
parent 34518 7407bc6cf28d (diff)
parent 34533 35308320713a (current diff)
child 34539 5d88e0681d44
merged, resolving minor conflicts;
src/Tools/jEdit/src/jedit/ProverSetup.scala
src/Tools/jEdit/src/jedit/TheoryView.scala
src/Tools/jEdit/src/proofdocument/ProofDocument.scala
src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/build.xml	Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/build.xml	Mon Mar 02 19:27:06 2009 +0100
@@ -72,4 +72,22 @@
       <copy file="plugin/actions.xml" todir="${build.classes.dir}" />
       <copy file="plugin/Isabelle.props" todir="${build.classes.dir}" />
     </target>
+    <target name="-post-jar">
+      <!-- jars -->
+      <delete file="${dist.dir}/jars/lib/jEdit.jar" />
+      <move todir="${dist.dir}/jars">
+        <fileset dir="${dist.dir}/jars/lib" />
+      </move>
+      <copy file="${scala.library}" todir="${dist.dir}/jars" />
+      <!-- clean up -->
+      <delete dir="{dist.dir}/jars/lib" />
+      <!-- dist-template -->
+      <copy file="dist-template/properties/jedit.props" tofile="${dist.dir}/properties" />
+      <copy todir="${dist.dir}/modes">
+        <fileset dir="dist-template/modes">
+          <exclude name="catalog-template" />
+        </fileset>
+      </copy>
+      <copy file="dist-template/modes/catalog-template" tofile="${dist.dir}/modes/catalog" />
+    </target>
 </project>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/modes/catalog-template	Mon Mar 02 19:27:06 2009 +0100
@@ -0,0 +1,10 @@
+<?xml version="1.0"?>
+<!DOCTYPE MODES SYSTEM "catalog.dtd">
+
+<MODES>
+
+<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy" />
+<MODE NAME="ml" FILE="ml.xml" FILE_NAME_GLOB="*.ML" />
+
+</MODES>
+
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Mon Mar 02 19:27:06 2009 +0100
@@ -7,6 +7,8 @@
 buffer.noTabs=true
 buffer.tabSize=2
 fallbackEncodings=US-ASCII ISO-8859-15
+firstTime=false
+tip.show=false
 encodingDetectors=BOM XML-PI buffer-local-property
 delete-line.shortcut=A+d
 delete.shortcut2=C+d
--- a/src/Tools/jEdit/makedist	Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/makedist	Mon Mar 02 19:27:06 2009 +0100
@@ -12,7 +12,6 @@
 ## diagnostics
 
 JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre16"
-SCALA_HOME="/home/scala/current"
 
 function usage()
 {
@@ -22,8 +21,6 @@
   echo "  Options are:"
   echo "    -j DIR       specify original jEdit distribution"
   echo "                 (default: $JEDIT_HOME)"
-  echo "    -s DIR       specify Scala distribution"
-  echo "                 (default: $SCALA_HOME)"
   echo
   echo "  Produce Isabelle/jEdit distribution from Netbeans build"
   echo "  in $THIS/dist"
@@ -48,9 +45,6 @@
     j)
       JEDIT_HOME="$OPTARG"
       ;;
-    s)
-      SCALA_HOME="$OPTARG"
-      ;;
     \?)
       usage
       ;;
@@ -86,10 +80,7 @@
 cp -R "$JEDIT_HOME/." "$JEDIT/."
 rm -rf "$JEDIT/jEdit" "$JEDIT/build-support"
 
-mkdir -p "$JEDIT/jars"
-
-[ "$SCALA_HOME/lib/scala-library.jar" ] || fail "Bad Scala directory: $SCALA_HOME"
-cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/"
+cp -R jars "$JEDIT/jars"
 
 cp -R "$THIS/dist-template/." "$JEDIT/."
 
@@ -97,13 +88,6 @@
   print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,; }
   print; }' "$JEDIT/modes/catalog"
 
-cp jars/Isabelle-jEdit.jar "$JEDIT/jars/isabelle.jar"
-cp jars/lib/Pure.jar "$JEDIT/jars/isabelle-Pure.jar"
-cp jars/lib/core-renderer.jar "$JEDIT/jars/"
-cp jars/lib/ErrorList.jar "$JEDIT/jars/"
-cp jars/lib/SideKick.jar "$JEDIT/jars/"
-
-
 # build archive
 
 echo "${JEDIT}.tar.gz"
--- a/src/Tools/jEdit/plugin/Isabelle.props	Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Mon Mar 02 19:27:06 2009 +0100
@@ -7,9 +7,9 @@
 plugin.isabelle.jedit.Plugin.description=Isabelle/Isar live document editing
 
 #system parameters
-plugin.isabelle.jedit.Plugin.activate=defer
+plugin.isabelle.jedit.Plugin.activate=startup
 plugin.isabelle.jedit.Plugin.usePluginHome=false
-plugin.isabelle.jedit.Plugin.jars=isabelle-Pure.jar core-renderer.jar scala-library.jar
+plugin.isabelle.jedit.Plugin.jars=Pure.jar core-renderer.jar scala-library.jar
 
 #dependencies
 plugin.isabelle.jedit.Plugin.depend.0=jdk 1.5
@@ -23,7 +23,7 @@
 options.isabelle.code=new isabelle.jedit.OptionPane();
 options.isabelle.font-path.title=Font Path
 options.isabelle.font-size.title=Font Size
-options.isabelle.font-size=14
+options.isabelle.font-size=18
 
 #menu actions
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Mon Mar 02 19:27:06 2009 +0100
@@ -1,50 +1,121 @@
 /*
  * include isabelle's command- and keyword-declarations
  * live in jEdits syntax-highlighting
- * 
- * one TokenMarker per prover
  *
  * @author Fabian Immler, TU Munich
  */
 
 package isabelle.jedit
 
-import org.gjt.sp.jedit.syntax.{ModeProvider, Token, TokenMarker, ParserRuleSet, KeywordMap}
+import isabelle.proofdocument.ProofDocument
+import isabelle.prover.{Command, MarkupNode}
+import isabelle.Markup
 
-class DynamicTokenMarker extends TokenMarker {
+import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.syntax._
 
-  val ruleset = new ParserRuleSet("isabelle", "MAIN")
+import java.awt.Color
+import java.awt.Font
+import javax.swing.text.Segment;
+
+object DynamicTokenMarker {
 
-  // copy rules and keywords from basic isabelle mode
-  val original = ModeProvider.instance.getMode("isabelle").getTokenMarker.getMainRuleSet
-  ruleset.addRuleSet(original)
-  ruleset.setKeywords(new KeywordMap(false))
-  ruleset.setDefault(0)
-  ruleset.setDigitRegexp(null)
-  ruleset.setEscapeRule(original.getEscapeRule)
-  ruleset.setHighlightDigits(false)
-  ruleset.setIgnoreCase(false)
-  ruleset.setNoWordSep("_'.?")
-  ruleset.setProperties(null)
-  ruleset.setTerminateChar(-1)
-
-  addRuleSet(ruleset)
+  def styles: Array[SyntaxStyle] = {
+    val array = new Array[SyntaxStyle](256)
+    // array(0) won't be used: reserved for global default-font
+    array(1) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font)
+    array(2) = new SyntaxStyle(new Color(255, 0, 255), Color.white, Isabelle.plugin.font)
+    array(3) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font)
+    array(4) = new SyntaxStyle(Color.green, Color.white, Isabelle.plugin.font)
+    array(5) = new SyntaxStyle(new Color(255, 128, 128), Color.white,Isabelle.plugin.font)
+    array(6) = new SyntaxStyle(Color.yellow, Color.white, Isabelle.plugin.font)
+    array(7) = new SyntaxStyle( new Color(0, 192, 0), Color.white, Isabelle.plugin.font)
+    array(8) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font)
+    array(9) = new SyntaxStyle(Color.green, Color.white, Isabelle.plugin.font)
+    array(10) = new SyntaxStyle(Color.gray, Color.white, Isabelle.plugin.font)
+    array(11) = new SyntaxStyle(Color.white, Color.white, Isabelle.plugin.font)
+    array(12) = new SyntaxStyle(Color.red, Color.white, Isabelle.plugin.font)
+    array(13) = new SyntaxStyle(Color.orange, Color.white, Isabelle.plugin.font)
+    return array
+  }
 
-  private val kinds = List(
-    OuterKeyword.minor -> Token.KEYWORD4,
-    OuterKeyword.control -> Token.INVALID,
-    OuterKeyword.diag -> Token.LABEL,
-    OuterKeyword.heading -> Token.KEYWORD1,
-    OuterKeyword.theory1 -> Token.KEYWORD4,
-    OuterKeyword.theory2 -> Token.KEYWORD1,
-    OuterKeyword.proof1 -> Token.KEYWORD1,
-    OuterKeyword.proof2 -> Token.KEYWORD2,
-    OuterKeyword.improper -> Token.DIGIT
-  )
-  def += (name: String, kind: String) = {
-    kinds.find(pair => pair._1.contains(kind)) match {
-      case None =>
-      case Some((_, kind_byte)) => getMainRuleSet.getKeywords.add(name, kind_byte)
+  def choose_byte(kind: String): Byte = {
+    // TODO: as properties
+    kind match {
+      // logical entities
+      case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL
+        | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT
+        | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => 2
+      // inner syntax
+      case Markup.TFREE | Markup.FREE => 3
+      case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => 4
+      case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL
+        | Markup.INNER_COMMENT => 5
+      case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
+        | Markup.ATTRIBUTE | Markup.METHOD => 6
+      // embedded source text
+      case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
+        | Markup.DOC_ANTIQ => 7
+      // outer syntax
+      case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => 8
+      case Markup.VERBATIM => 9
+      case Markup.COMMENT => 10
+      case Markup.CONTROL => 11
+      case Markup.MALFORMED => 12
+      case Markup.STRING | Markup.ALTSTRING => 13
+      // other
+      case _ => 1
     }
   }
+
+  def choose_color(kind : String) : Color = styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor
+
 }
+
+class DynamicTokenMarker(buffer: JEditBuffer, document: ProofDocument) extends TokenMarker {
+
+  override def markTokens(prev: TokenMarker.LineContext,
+    handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = {
+    val previous = prev.asInstanceOf[IndexLineContext]
+    val line = if(prev == null) 0 else previous.line + 1
+    val context = new IndexLineContext(line, previous)
+    val start = buffer.getLineStartOffset(line)
+    val stop = start + line_segment.count
+    
+    def to = Isabelle.prover_setup(buffer).get.theory_view.to_current(_)
+    def from = Isabelle.prover_setup(buffer).get.theory_view.from_current(_)
+
+    val commands = document.commands.dropWhile(_.stop <= from(start))
+    if(commands.hasNext) {
+      var next_x = start
+      for {
+        command <- commands.takeWhile(_.start < from(stop))
+        markup <- command.root_node.flatten
+        if(to(markup.abs_stop) > start)
+        if(to(markup.abs_start) < stop)
+        byte = DynamicTokenMarker.choose_byte(markup.kind)
+        token_start = to(markup.abs_start) - start max 0
+        token_length = to(markup.abs_stop) - to(markup.abs_start) -
+                       (start - to(markup.abs_start) max 0) -
+                       (to(markup.abs_stop) - stop max 0)
+      } {
+        if (start + token_start > next_x) 
+          handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
+        handler.handleToken(line_segment, byte, token_start, token_length, context)
+        next_x = start + token_start + token_length
+      }
+      if (next_x < stop)
+        handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
+    } else {
+      handler.handleToken(line_segment, 1, 0, line_segment.count, context)
+    }
+
+    handler.handleToken(line_segment,Token.END, line_segment.count, 0, context)
+    handler.setLineContext(context)
+    return context
+  }
+
+}
+
+class IndexLineContext(val line: Int, prev: IndexLineContext)
+  extends TokenMarker.LineContext(new ParserRuleSet("isabelle", "MAIN"), prev)
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Mar 02 19:27:06 2009 +0100
@@ -17,7 +17,7 @@
 import org.gjt.sp.jedit.buffer.JEditBuffer;
 import org.gjt.sp.jedit._
 
-class PhaseOverviewPanel(prover : isabelle.prover.Prover) extends JPanel(new BorderLayout) {
+class PhaseOverviewPanel(prover: isabelle.prover.Prover, to_current: Int => Int) extends JPanel(new BorderLayout) {
 
   private val WIDTH = 10
 	private val HILITE_HEIGHT = 2
@@ -25,7 +25,7 @@
 
   val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
   prover.command_info += (_ => repaint_delay.delay_or_ignore())
-    
+
   setRequestFocusEnabled(false);
 
   addMouseListener(new MouseAdapter {
@@ -59,8 +59,8 @@
 	}
 
   private def paintCommand(command : Command, buffer : JEditBuffer, gfx : Graphics) {
-      val line1 = buffer.getLineOfOffset(command.start)
-      val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
+      val line1 = buffer.getLineOfOffset(to_current(command.start))
+      val line2 = buffer.getLineOfOffset(to_current(command.stop - 1)) + 1
       val y = lineToY(line1)
       val height = lineToY(line2) - y - 1
       val (light, dark) = command.status match {
@@ -84,7 +84,7 @@
 		val buffer = textarea.getBuffer
     for (c <- prover.document.commands)
       paintCommand(c, buffer, gfx)
-    
+
 	}
 
 	override def getPreferredSize : Dimension =
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Mon Mar 02 19:27:06 2009 +0100
@@ -35,7 +35,7 @@
 
   def activate(view: View) {
     prover = new Prover(Isabelle.system, Isabelle.default_logic)
-    
+
     val buffer = view.getBuffer
     val path = buffer.getPath
 
@@ -73,13 +73,6 @@
           state_panel.setDocument(state.result_document, UserAgent.baseURL)
       }
     })
-  
-    // one independent token marker per prover
-    val token_marker = new DynamicTokenMarker
-    buffer.setTokenMarker(token_marker)
-
-    // register for new declarations
-    prover.decl_info += (pair => token_marker += (pair._1, pair._2))
 
   }
 
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Mar 02 19:27:06 2009 +0100
@@ -35,35 +35,6 @@
         case _ => Color.red
       }
   }
-
-  def choose_color(markup: String): Color = {
-    // TODO: as properties
-    markup match {
-      // logical entities
-      case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL
-        | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT
-        | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => new Color(255, 0, 255)
-      // inner syntax
-      case Markup.TFREE | Markup.FREE => Color.blue
-      case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => Color.green
-      case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL
-        | Markup.INNER_COMMENT => new Color(255, 128, 128)
-      case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
-        | Markup.ATTRIBUTE | Markup.METHOD => Color.yellow
-      // embedded source text
-      case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
-        | Markup.DOC_ANTIQ => new Color(0, 192, 0)
-      // outer syntax
-      case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => Color.blue
-      case Markup.VERBATIM => Color.green
-      case Markup.COMMENT => Color.gray
-      case Markup.CONTROL => Color.white
-      case Markup.MALFORMED => Color.red
-      case Markup.STRING | Markup.ALTSTRING => Color.orange
-      // other
-      case _ => Color.white
-    }
-  }
 }
 
 
@@ -78,29 +49,25 @@
   private var col: Text.Changed = null
 
   private val col_timer = new Timer(300, new ActionListener() {
-    override def actionPerformed(e: ActionEvent) = commit()
+    override def actionPerformed(e: ActionEvent) = commit
   })
 
   col_timer.stop
   col_timer.setRepeats(true)
 
 
-  private val phase_overview = new PhaseOverviewPanel(prover)
+  private val phase_overview = new PhaseOverviewPanel(prover, to_current(_))
 
 
   /* activation */
 
-  Isabelle.plugin.font_changed += (_ => update_font())
+  Isabelle.plugin.font_changed += (_ => update_styles)
 
-  private def update_font() = {
+  private def update_styles = {
     if (text_area != null) {
       if (Isabelle.plugin.font != null) {
-        val painter = text_area.getPainter
-        painter.setStyles(painter.getStyles.map(style =>
-          new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, Isabelle.plugin.font)
-        ))
-        painter.setFont(Isabelle.plugin.font)
-        repaint_all()
+        text_area.getPainter.setStyles(DynamicTokenMarker.styles)
+        repaint_all
       }
     }
   }
@@ -119,7 +86,8 @@
     phase_overview.textarea = text_area
     text_area.addLeftOfScrollBar(phase_overview)
     text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
-    update_font()
+    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover.document))
+    update_styles
   }
 
   def deactivate() = {
@@ -134,13 +102,13 @@
   val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
   prover.command_info += (_ => repaint_delay.delay_or_ignore())
 
-  private def from_current(pos: Int) =
+  def from_current (pos: Int) =
     if (col != null && col.start <= pos)
       if (pos < col.start + col.added) col.start
       else pos - col.added + col.removed
     else pos
 
-  private def to_current(pos : Int) =
+  def to_current (pos : Int) =
     if (col != null && col.start <= pos)
       if (pos < col.start + col.removed) col.start
       else pos + col.added - col.removed
@@ -172,7 +140,8 @@
       if (finish < buffer.getLength) text_area.offsetToXY(finish)
       else {
         val p = text_area.offsetToXY(finish - 1)
-        p.x = p.x + text_area.getPainter.getFontMetrics.charWidth(' ')
+        val metrics = text_area.getPainter.getFontMetrics
+        p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
         p
       }
 
@@ -203,10 +172,10 @@
       // paint details of command
       for (node <- e.root_node.dfs) {
         val begin = to_current(node.start + e.start)
-        val finish = to_current(node.end + e.start)
+        val finish = to_current(node.stop + e.start)
         if (finish > start && begin < end) {
-          encolor(gfx, y + metrics.getHeight - 4, 2, begin max start, finish min end,
-            TheoryView.choose_color(node.short), true)
+          encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1,
+            DynamicTokenMarker.choose_color(node.kind), true)
         }
       }
       e = e.next
@@ -225,7 +194,7 @@
 
   /* BufferListener methods */
 
-  private def commit() {
+  private def commit {
     if (col != null)
       changes.event(col)
     col = null
@@ -233,7 +202,7 @@
       col_timer.stop()
   }
 
-  private def delay_commit() {
+  private def delay_commit {
     if (col_timer.isRunning())
       col_timer.restart()
     else
@@ -250,10 +219,10 @@
     else if (col.start <= offset && offset <= col.start + col.added)
       col = new Text.Changed(col.start, col.added + length, col.removed)
     else {
-      commit()
+      commit
       col = new Text.Changed(offset, length, 0)
     }
-    delay_commit()
+    delay_commit
 */
     changes.event(new Text.Changed(offset, length, 0))
   }
@@ -265,7 +234,7 @@
     if (col == null)
       col = new Text.Changed(start, 0, removed)
     else if (col.start > start + removed || start > col.start + col.added) {
-      commit()
+      commit
       col = new Text.Changed(start, 0, removed)
     }
     else {
@@ -278,7 +247,7 @@
           (diff - (offset min 0), offset min 0)
       col = new Text.Changed(start min col.start, added, col.removed - add_removed)
     }
-    delay_commit()
+    delay_commit
 */
     changes.event(new Text.Changed(start, 0, removed))
   }
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Mar 02 19:27:06 2009 +0100
@@ -230,11 +230,13 @@
 
   val structural_changes = new EventBus[StructureChange]
 
-  def commands = new Iterator[Command] {
-    var current = first_token
+  def commands_from(start: Token) = new Iterator[Command] {
+    var current = start
     def hasNext = current != null
-    def next() = { val s = current.command ; current = s.last.next ; s }
+    def next = { val s = current.command ; current = s.last.next ; s }
   }
+  def commands_from(start: Command): Iterator[Command] = commands_from(start.first)
+  def commands = commands_from(first_token)
 
   def find_command_at(pos: Int): Command = {
     for (cmd <- commands) { if (pos < cmd.stop) return cmd }
--- a/src/Tools/jEdit/src/prover/Command.scala	Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Mon Mar 02 19:27:06 2009 +0100
@@ -104,7 +104,7 @@
     new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)
 
   def node_from(kind: String, begin: Int, end: Int) = {
-    val markup_content = /*content.substring(begin, end)*/ ""
+    val markup_content = content.substring(begin, end)
     new MarkupNode(this, begin, end, id, kind, markup_content)
   }
 }
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Mon Mar 02 19:17:20 2009 +0100
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Mon Mar 02 19:27:06 2009 +0100
@@ -20,29 +20,33 @@
 
     object RelativeAsset extends IAsset {
       override def getIcon : Icon = null
-      override def getShortString : String = node.short
-      override def getLongString : String = node.long
-      override def getName : String = node.name
-      override def setName(name : String) = ()
+      override def getShortString : String = node.kind
+      override def getLongString : String = node.desc
+      override def getName : String = node.id
+      override def setName (name : String) = ()
       override def setStart(start : Position) = ()
-      override def getStart : Position = node.base.start + node.start
+      override def getStart : Position = node.abs_start
       override def setEnd(end : Position) = ()
-      override def getEnd : Position = node.base.start + node.end
-      override def toString = node.name + ": " + node.short
+      override def getEnd : Position = node.abs_stop
+      override def toString = node.id + ": " + node.kind + "[" + node.start + " - " + node.stop + "]"
     }
 
     new DefaultMutableTreeNode(RelativeAsset)
   }
 }
 
-class MarkupNode (val base : Command, val start : Int, val end : Int,
-                    val name : String, val short : String, val long : String) {
+class MarkupNode (val base : Command, val start : Int, val stop : Int,
+                    val id : String, val kind : String, val desc : String) {
 
   val swing_node : DefaultMutableTreeNode = MarkupNode.markup2default_node (this)
 
   var parent : MarkupNode = null
   def orphan = parent == null
 
+  def length = stop - start
+  def abs_start = base.start + start
+  def abs_stop = base.start + stop
+
   private var children_cell : List[MarkupNode] = Nil
   //track changes in swing_node
   def children = children_cell
@@ -51,10 +55,10 @@
     for (c <- cs) swing_node add c.swing_node
     children_cell = cs
   }
-  
+
   private def add(child : MarkupNode) {
     child parent = this
-    children_cell = (child :: children) sort ((a, b) => a.start < b.end)
+    children_cell = (child :: children) sort ((a, b) => a.start < b.start)
 
     swing_node add child.swing_node
   }
@@ -78,6 +82,28 @@
     all
   }
 
+  def leafs: List[MarkupNode] = {
+    if (children == Nil) return List(this)
+    else return children flatMap (_.leafs)
+  }
+
+  def flatten: List[MarkupNode] = {
+    var next_x = start
+    if(children.length == 0) List(this)
+    else {
+      val filled_gaps = for {
+        child <- children
+        markups = if (next_x < child.start) {
+          new MarkupNode(base, next_x, child.start, id, kind, "") :: child.flatten
+        } else child.flatten
+        update = (next_x = child.stop)
+        markup <- markups
+      } yield markup
+      if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, id, kind, "")
+      else filled_gaps
+    }
+  }
+
   def insert(new_child : MarkupNode) : Unit = {
     if (new_child fitting_into this) {
       for (child <- children) {
@@ -96,13 +122,14 @@
         this remove new_child.children
       }
     } else {
-      System.err.println("ignored nonfitting markup " + new_child.name + new_child.short + new_child.long
-                         + "(" +new_child.start + ", "+ new_child.end + ")")
+      System.err.println("ignored nonfitting markup " + new_child.id + new_child.kind + new_child.desc
+                         + "(" +new_child.start + ", "+ new_child.stop + ")")
     }
   }
 
   // does this fit into node?
   def fitting_into(node : MarkupNode) = node.start <= this.start &&
-    node.end >= this.end
-  
+    node.stop >= this.stop
+
+  override def toString = "([" + start + " - " + stop + "] " + id + "( " + kind + "): " + desc
 }