misc rearrangement of files;
authorwenzelm
Tue Dec 08 14:49:01 2009 +0100 (2009-12-08)
changeset 34759bfea7839d9e1
parent 34758 710e3a9a4c95
child 34760 dc7f5e0d9d27
misc rearrangement of files;
src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala
src/Tools/jEdit/src/jedit/Document_Overview.scala
src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
src/Tools/jEdit/src/jedit/Isabelle_Encoding.scala
src/Tools/jEdit/src/jedit/OptionPane.scala
src/Tools/jEdit/src/jedit/OutputDockable.scala
src/Tools/jEdit/src/jedit/Plugin.scala
src/Tools/jEdit/src/jedit/ProverSetup.scala
src/Tools/jEdit/src/jedit/StateViewDockable.scala
src/Tools/jEdit/src/jedit/TheoryView.scala
src/Tools/jEdit/src/jedit/browse_version_dockable.scala
src/Tools/jEdit/src/jedit/document_overview.scala
src/Tools/jEdit/src/jedit/isabelle_encoding.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit/option_pane.scala
src/Tools/jEdit/src/jedit/plugin.scala
src/Tools/jEdit/src/jedit/prover_setup.scala
src/Tools/jEdit/src/jedit/raw_output_dockable.scala
src/Tools/jEdit/src/jedit/results_dockable.scala
src/Tools/jEdit/src/jedit/token_marker.scala
src/Tools/jEdit/src/proofdocument/Change.scala
src/Tools/jEdit/src/proofdocument/ProofDocument.scala
src/Tools/jEdit/src/proofdocument/Token.scala
src/Tools/jEdit/src/proofdocument/change.scala
src/Tools/jEdit/src/proofdocument/command.scala
src/Tools/jEdit/src/proofdocument/markup_node.scala
src/Tools/jEdit/src/proofdocument/proof_document.scala
src/Tools/jEdit/src/proofdocument/prover.scala
src/Tools/jEdit/src/proofdocument/state.scala
src/Tools/jEdit/src/proofdocument/theory_view.scala
src/Tools/jEdit/src/proofdocument/token.scala
src/Tools/jEdit/src/prover/Command.scala
src/Tools/jEdit/src/prover/MarkupNode.scala
src/Tools/jEdit/src/prover/Prover.scala
src/Tools/jEdit/src/prover/State.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala	Tue Dec 08 14:29:29 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,43 +0,0 @@
     1.4 -/*
     1.5 - * Dockable window for navigating through the document-versions
     1.6 - *
     1.7 - * @author Fabian Immler, TU Munich
     1.8 - */
     1.9 -
    1.10 -package isabelle.jedit
    1.11 -
    1.12 -import isabelle.proofdocument.Change
    1.13 -
    1.14 -import java.awt.Dimension
    1.15 -import scala.swing.{ListView, FlowPanel}
    1.16 -import scala.swing.event.ListSelectionChanged
    1.17 -
    1.18 -import org.gjt.sp.jedit.View
    1.19 -import org.gjt.sp.jedit.gui.DockableWindowManager
    1.20 -
    1.21 -
    1.22 -class BrowseVersionDockable(view: View, position: String) extends FlowPanel
    1.23 -{
    1.24 -  if (position == DockableWindowManager.FLOATING)
    1.25 -    preferredSize = new Dimension(500, 250)
    1.26 -
    1.27 -  def prover_setup(): Option[ProverSetup] = Isabelle.prover_setup(view.getBuffer)
    1.28 -  def get_versions() =
    1.29 -    prover_setup() match {
    1.30 -      case None => Nil
    1.31 -      case Some(setup) => setup.theory_view.changes
    1.32 -    }
    1.33 -
    1.34 -  val list = new ListView[Change]
    1.35 -  list.fixedCellWidth = 500
    1.36 -  list.listData = get_versions()
    1.37 -  contents += list
    1.38 -
    1.39 -  listenTo(list.selection)
    1.40 -  reactions += {
    1.41 -    case ListSelectionChanged(source, range, false) =>
    1.42 -        prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
    1.43 -    }
    1.44 -
    1.45 -  prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
    1.46 -}
     2.1 --- a/src/Tools/jEdit/src/jedit/Document_Overview.scala	Tue Dec 08 14:29:29 2009 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,82 +0,0 @@
     2.4 -/*
     2.5 - * Information on command status left of scrollbar (with panel)
     2.6 - *
     2.7 - * @author Fabian Immler, TU Munich
     2.8 - */
     2.9 -
    2.10 -package isabelle.jedit
    2.11 -
    2.12 -import isabelle.prover.{Prover, Command}
    2.13 -import isabelle.proofdocument.ProofDocument
    2.14 -
    2.15 -import javax.swing.{JPanel, ToolTipManager}
    2.16 -import java.awt.event.{MouseAdapter, MouseEvent}
    2.17 -import java.awt.{BorderLayout, Graphics, Dimension}
    2.18 -
    2.19 -import org.gjt.sp.jedit.gui.RolloverButton
    2.20 -import org.gjt.sp.jedit.textarea.JEditTextArea
    2.21 -import org.gjt.sp.jedit.buffer.JEditBuffer
    2.22 -
    2.23 -
    2.24 -class Document_Overview(
    2.25 -    prover: Prover,
    2.26 -    text_area: JEditTextArea,
    2.27 -    to_current: (ProofDocument, Int) => Int)
    2.28 -  extends JPanel(new BorderLayout)
    2.29 -{
    2.30 -  private val WIDTH = 10
    2.31 -  private val HEIGHT = 2
    2.32 -
    2.33 -  setRequestFocusEnabled(false)
    2.34 -
    2.35 -  addMouseListener(new MouseAdapter {
    2.36 -    override def mousePressed(event: MouseEvent) {
    2.37 -      val line = y_to_line(event.getY)
    2.38 -      if (line >= 0 && line < text_area.getLineCount)
    2.39 -        text_area.setCaretPosition(text_area.getLineStartOffset(line))
    2.40 -    }
    2.41 -  })
    2.42 -
    2.43 -  override def addNotify() {
    2.44 -    super.addNotify()
    2.45 -    ToolTipManager.sharedInstance.registerComponent(this)
    2.46 -  }
    2.47 -
    2.48 -  override def removeNotify() {
    2.49 -    super.removeNotify
    2.50 -    ToolTipManager.sharedInstance.unregisterComponent(this)
    2.51 -  }
    2.52 -
    2.53 -  override def getToolTipText(event: MouseEvent): String =
    2.54 -  {
    2.55 -    val buffer = text_area.getBuffer
    2.56 -    val lineCount = buffer.getLineCount
    2.57 -    val line = y_to_line(event.getY())
    2.58 -    if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
    2.59 -    else ""
    2.60 -  }
    2.61 -
    2.62 -  override def paintComponent(gfx: Graphics) {
    2.63 -    super.paintComponent(gfx)
    2.64 -    val buffer = text_area.getBuffer
    2.65 -    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
    2.66 -    val doc = theory_view.current_document()
    2.67 -
    2.68 -    for (command <- doc.commands) {
    2.69 -      val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc)))
    2.70 -      val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1
    2.71 -      val y = line_to_y(line1)
    2.72 -      val height = HEIGHT * (line2 - line1)
    2.73 -      gfx.setColor(TheoryView.choose_color(command, doc))
    2.74 -      gfx.fillRect(0, y, getWidth - 1, height)
    2.75 -    }
    2.76 -  }
    2.77 -
    2.78 -  override def getPreferredSize = new Dimension(WIDTH, 0)
    2.79 -
    2.80 -  private def line_to_y(line: Int): Int =
    2.81 -    (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
    2.82 -
    2.83 -  private def y_to_line(y: Int): Int =
    2.84 -    (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
    2.85 -}
    2.86 \ No newline at end of file
     3.1 --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Tue Dec 08 14:29:29 2009 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,154 +0,0 @@
     3.4 -/*
     3.5 - * include isabelle's command- and keyword-declarations
     3.6 - * live in jEdits syntax-highlighting
     3.7 - *
     3.8 - * @author Fabian Immler, TU Munich
     3.9 - */
    3.10 -
    3.11 -package isabelle.jedit
    3.12 -
    3.13 -
    3.14 -import isabelle.prover.Prover
    3.15 -import isabelle.Markup
    3.16 -
    3.17 -import org.gjt.sp.jedit.buffer.JEditBuffer
    3.18 -import org.gjt.sp.jedit.syntax.{Token => JToken,
    3.19 -  TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
    3.20 -
    3.21 -import java.awt.Color
    3.22 -import java.awt.Font
    3.23 -import javax.swing.text.Segment;
    3.24 -
    3.25 -
    3.26 -object DynamicTokenMarker
    3.27 -{
    3.28 -  /* line context */
    3.29 -
    3.30 -  private val rule_set = new ParserRuleSet("isabelle", "MAIN")
    3.31 -  private class LineContext(val line: Int, prev: LineContext)
    3.32 -    extends TokenMarker.LineContext(rule_set, prev)
    3.33 -
    3.34 -
    3.35 -  /* mapping to jEdit token types */
    3.36 -  // TODO: as properties or CSS style sheet
    3.37 -
    3.38 -  private val choose_byte: Map[String, Byte] =
    3.39 -  {
    3.40 -    import JToken._
    3.41 -    Map[String, Byte](
    3.42 -      // logical entities
    3.43 -      Markup.TCLASS -> LABEL,
    3.44 -      Markup.TYCON -> LABEL,
    3.45 -      Markup.FIXED_DECL -> LABEL,
    3.46 -      Markup.FIXED -> LABEL,
    3.47 -      Markup.CONST_DECL -> LABEL,
    3.48 -      Markup.CONST -> LABEL,
    3.49 -      Markup.FACT_DECL -> LABEL,
    3.50 -      Markup.FACT -> LABEL,
    3.51 -      Markup.DYNAMIC_FACT -> LABEL,
    3.52 -      Markup.LOCAL_FACT_DECL -> LABEL,
    3.53 -      Markup.LOCAL_FACT -> LABEL,
    3.54 -      // inner syntax
    3.55 -      Markup.TFREE -> LITERAL2,
    3.56 -      Markup.FREE -> LITERAL2,
    3.57 -      Markup.TVAR -> LITERAL3,
    3.58 -      Markup.SKOLEM -> LITERAL3,
    3.59 -      Markup.BOUND -> LITERAL3,
    3.60 -      Markup.VAR -> LITERAL3,
    3.61 -      Markup.NUM -> DIGIT,
    3.62 -      Markup.FLOAT -> DIGIT,
    3.63 -      Markup.XNUM -> DIGIT,
    3.64 -      Markup.XSTR -> LITERAL4,
    3.65 -      Markup.LITERAL -> LITERAL4,
    3.66 -      Markup.INNER_COMMENT -> COMMENT1,
    3.67 -      Markup.SORT -> FUNCTION,
    3.68 -      Markup.TYP -> FUNCTION,
    3.69 -      Markup.TERM -> FUNCTION,
    3.70 -      Markup.PROP -> FUNCTION,
    3.71 -      Markup.ATTRIBUTE -> FUNCTION,
    3.72 -      Markup.METHOD -> FUNCTION,
    3.73 -      // ML syntax
    3.74 -      Markup.ML_KEYWORD -> KEYWORD2,
    3.75 -      Markup.ML_IDENT -> NULL,
    3.76 -      Markup.ML_TVAR -> LITERAL3,
    3.77 -      Markup.ML_NUMERAL -> DIGIT,
    3.78 -      Markup.ML_CHAR -> LITERAL1,
    3.79 -      Markup.ML_STRING -> LITERAL1,
    3.80 -      Markup.ML_COMMENT -> COMMENT1,
    3.81 -      Markup.ML_MALFORMED -> INVALID,
    3.82 -      // embedded source text
    3.83 -      Markup.ML_SOURCE -> COMMENT4,
    3.84 -      Markup.DOC_SOURCE -> COMMENT4,
    3.85 -      Markup.ANTIQ -> COMMENT4,
    3.86 -      Markup.ML_ANTIQ -> COMMENT4,
    3.87 -      Markup.DOC_ANTIQ -> COMMENT4,
    3.88 -      // outer syntax
    3.89 -      Markup.IDENT -> NULL,
    3.90 -      Markup.COMMAND -> OPERATOR,
    3.91 -      Markup.KEYWORD -> KEYWORD4,
    3.92 -      Markup.VERBATIM -> COMMENT3,
    3.93 -      Markup.COMMENT -> COMMENT1,
    3.94 -      Markup.CONTROL -> COMMENT3,
    3.95 -      Markup.MALFORMED -> INVALID,
    3.96 -      Markup.STRING -> LITERAL3,
    3.97 -      Markup.ALTSTRING -> LITERAL1
    3.98 -    ).withDefaultValue(NULL)
    3.99 -  }
   3.100 -
   3.101 -  def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
   3.102 -    styles(choose_byte(kind)).getForegroundColor
   3.103 -}
   3.104 -
   3.105 -
   3.106 -class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover)
   3.107 -  extends TokenMarker
   3.108 -{
   3.109 -  override def markTokens(prev: TokenMarker.LineContext,
   3.110 -      handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
   3.111 -  {
   3.112 -    val previous = prev.asInstanceOf[DynamicTokenMarker.LineContext]
   3.113 -    val line = if (prev == null) 0 else previous.line + 1
   3.114 -    val context = new DynamicTokenMarker.LineContext(line, previous)
   3.115 -    val start = buffer.getLineStartOffset(line)
   3.116 -    val stop = start + line_segment.count
   3.117 -
   3.118 -    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
   3.119 -    val document = theory_view.current_document()
   3.120 -    def to: Int => Int = theory_view.to_current(document, _)
   3.121 -    def from: Int => Int = theory_view.from_current(document, _)
   3.122 -
   3.123 -    var next_x = start
   3.124 -    var cmd = document.command_at(from(start))
   3.125 -    while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
   3.126 -      val command = cmd.get
   3.127 -      for {
   3.128 -        markup <- command.highlight(document).flatten
   3.129 -        command_start = command.start(document)
   3.130 -        abs_start = to(command_start + markup.start)
   3.131 -        abs_stop = to(command_start + markup.stop)
   3.132 -        if (abs_stop > start)
   3.133 -        if (abs_start < stop)
   3.134 -        byte = DynamicTokenMarker.choose_byte(markup.info.toString)
   3.135 -        token_start = (abs_start - start) max 0
   3.136 -        token_length =
   3.137 -          (abs_stop - abs_start) -
   3.138 -          ((start - abs_start) max 0) -
   3.139 -          ((abs_stop - stop) max 0)
   3.140 -      } {
   3.141 -        if (start + token_start > next_x)
   3.142 -          handler.handleToken(line_segment, 1,
   3.143 -            next_x - start, start + token_start - next_x, context)
   3.144 -        handler.handleToken(line_segment, byte,
   3.145 -          token_start, token_length, context)
   3.146 -        next_x = start + token_start + token_length
   3.147 -      }
   3.148 -      cmd = document.commands.next(command)
   3.149 -    }
   3.150 -    if (next_x < stop)
   3.151 -      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
   3.152 -
   3.153 -    handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
   3.154 -    handler.setLineContext(context)
   3.155 -    return context
   3.156 -  }
   3.157 -}
     4.1 --- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Tue Dec 08 14:29:29 2009 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,80 +0,0 @@
     4.4 -/*
     4.5 - * Hyperlink setup for Isabelle proof documents
     4.6 - *
     4.7 - * @author Fabian Immler, TU Munich
     4.8 - */
     4.9 -
    4.10 -package isabelle.jedit
    4.11 -
    4.12 -import java.io.File
    4.13 -
    4.14 -import gatchan.jedit.hyperlinks.Hyperlink
    4.15 -import gatchan.jedit.hyperlinks.HyperlinkSource
    4.16 -import gatchan.jedit.hyperlinks.AbstractHyperlink
    4.17 -
    4.18 -import org.gjt.sp.jedit.View
    4.19 -import org.gjt.sp.jedit.jEdit
    4.20 -import org.gjt.sp.jedit.Buffer
    4.21 -import org.gjt.sp.jedit.TextUtilities
    4.22 -
    4.23 -import isabelle.prover.Command
    4.24 -
    4.25 -
    4.26 -class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
    4.27 -  extends AbstractHyperlink(start, end, line, "")
    4.28 -{
    4.29 -  override def click(view: View) {
    4.30 -    view.getTextArea.moveCaretPosition(ref_offset)
    4.31 -  }
    4.32 -}
    4.33 -
    4.34 -class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
    4.35 -  extends AbstractHyperlink(start, end, line, "")
    4.36 -{
    4.37 -  override def click(view: View) = {
    4.38 -    Isabelle.system.source_file(ref_file) match {
    4.39 -      case None => System.err.println("Could not find source file " + ref_file)
    4.40 -      case Some(file) =>
    4.41 -        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
    4.42 -    }
    4.43 -  }
    4.44 -}
    4.45 -
    4.46 -class IsabelleHyperlinkSource extends HyperlinkSource
    4.47 -{
    4.48 -	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
    4.49 -    val prover = Isabelle.prover_setup(buffer).map(_.prover)
    4.50 -    val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
    4.51 -    if (prover.isEmpty || theory_view_opt.isEmpty) null
    4.52 -    else if (prover.get == null || theory_view_opt.get == null) null
    4.53 -    else {
    4.54 -      val theory_view = theory_view_opt.get
    4.55 -      val document = theory_view.current_document()
    4.56 -      val offset = theory_view.from_current(document, original_offset)
    4.57 -      document.command_at(offset) match {
    4.58 -        case Some(command) =>
    4.59 -          command.ref_at(document, offset - command.start(document)) match {
    4.60 -            case Some(ref) =>
    4.61 -              val command_start = command.start(document)
    4.62 -              val begin = theory_view.to_current(document, command_start + ref.start)
    4.63 -              val line = buffer.getLineOfOffset(begin)
    4.64 -              val end = theory_view.to_current(document, command_start + ref.stop)
    4.65 -              ref.info match {
    4.66 -                case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
    4.67 -                  new ExternalHyperlink(begin, end, line, ref_file, ref_line)
    4.68 -                case Command.RefInfo(_, _, Some(id), Some(offset)) =>
    4.69 -                  prover.get.command(id) match {
    4.70 -                    case Some(ref_cmd) =>
    4.71 -                      new InternalHyperlink(begin, end, line,
    4.72 -                        theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
    4.73 -                    case None => null
    4.74 -                  }
    4.75 -                case _ => null
    4.76 -              }
    4.77 -            case None => null
    4.78 -          }
    4.79 -        case None => null
    4.80 -      }
    4.81 -    }
    4.82 -  }
    4.83 -}
     5.1 --- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Tue Dec 08 14:29:29 2009 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,102 +0,0 @@
     5.4 -/*
     5.5 - * SideKick parser for Isabelle proof documents
     5.6 - *
     5.7 - * @author Fabian Immler, TU Munich
     5.8 - * @author Makarius
     5.9 - */
    5.10 -
    5.11 -package isabelle.jedit
    5.12 -
    5.13 -import scala.collection.Set
    5.14 -import scala.collection.immutable.TreeSet
    5.15 -
    5.16 -import javax.swing.tree.DefaultMutableTreeNode
    5.17 -import javax.swing.text.Position
    5.18 -import javax.swing.Icon
    5.19 -
    5.20 -import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
    5.21 -import errorlist.DefaultErrorSource
    5.22 -import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
    5.23 -
    5.24 -import isabelle.prover.{Command, Markup_Node}
    5.25 -import isabelle.proofdocument.ProofDocument
    5.26 -
    5.27 -
    5.28 -class IsabelleSideKickParser extends SideKickParser("isabelle")
    5.29 -{
    5.30 -  /* parsing */
    5.31 -
    5.32 -  @volatile private var stopped = false
    5.33 -  override def stop() = { stopped = true }
    5.34 -
    5.35 -  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
    5.36 -  {
    5.37 -    implicit def int_to_pos(offset: Int): Position =
    5.38 -      new Position { def getOffset = offset; override def toString = offset.toString }
    5.39 -
    5.40 -    stopped = false
    5.41 -
    5.42 -    val data = new SideKickParsedData(buffer.getName)
    5.43 -    val root = data.root
    5.44 -    data.getAsset(root).setEnd(buffer.getLength)
    5.45 -
    5.46 -    val prover_setup = Isabelle.prover_setup(buffer)
    5.47 -    if (prover_setup.isDefined) {
    5.48 -      val document = prover_setup.get.theory_view.current_document()
    5.49 -      for (command <- document.commands if !stopped) {
    5.50 -        root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
    5.51 -            {
    5.52 -              val content = command.content(node.start, node.stop)
    5.53 -              val command_start = command.start(document)
    5.54 -              val id = command.id
    5.55 -
    5.56 -              new DefaultMutableTreeNode(new IAsset {
    5.57 -                override def getIcon: Icon = null
    5.58 -                override def getShortString: String = content
    5.59 -                override def getLongString: String = node.info.toString
    5.60 -                override def getName: String = id
    5.61 -                override def setName(name: String) = ()
    5.62 -                override def setStart(start: Position) = ()
    5.63 -                override def getStart: Position = command_start + node.start
    5.64 -                override def setEnd(end: Position) = ()
    5.65 -                override def getEnd: Position = command_start + node.stop
    5.66 -                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
    5.67 -              })
    5.68 -            }))
    5.69 -      }
    5.70 -      if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
    5.71 -    }
    5.72 -    else root.add(new DefaultMutableTreeNode("<buffer inactive>"))
    5.73 -
    5.74 -    data
    5.75 -  }
    5.76 -
    5.77 -
    5.78 -  /* completion */
    5.79 -
    5.80 -  override def supportsCompletion = true
    5.81 -  override def canCompleteAnywhere = true
    5.82 -
    5.83 -  override def complete(pane: EditPane, caret: Int): SideKickCompletion =
    5.84 -  {
    5.85 -    val buffer = pane.getBuffer
    5.86 -
    5.87 -    val line = buffer.getLineOfOffset(caret)
    5.88 -    val start = buffer.getLineStartOffset(line)
    5.89 -    val text = buffer.getSegment(start, caret - start)
    5.90 -
    5.91 -    val completion =
    5.92 -      Isabelle.prover_setup(buffer).map(_.prover.completion()).getOrElse(Isabelle.completion)
    5.93 -
    5.94 -    completion.complete(text) match {
    5.95 -      case None => null
    5.96 -      case Some((word, cs)) =>
    5.97 -        val ds =
    5.98 -          if (Isabelle_Encoding.is_active(buffer))
    5.99 -            cs.map(Isabelle.system.symbols.decode(_)).sort(Completion.length_ord _)
   5.100 -          else cs
   5.101 -        new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
   5.102 -    }
   5.103 -  }
   5.104 -
   5.105 -}
     6.1 --- a/src/Tools/jEdit/src/jedit/Isabelle_Encoding.scala	Tue Dec 08 14:29:29 2009 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,63 +0,0 @@
     6.4 -/*
     6.5 - * Isabelle encoding -- based on utf-8
     6.6 - *
     6.7 - * @author Makarius
     6.8 - */
     6.9 -
    6.10 -package isabelle.jedit
    6.11 -
    6.12 -import org.gjt.sp.jedit.io.Encoding
    6.13 -import org.gjt.sp.jedit.buffer.JEditBuffer
    6.14 -
    6.15 -import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
    6.16 -import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
    6.17 -  CharArrayReader, ByteArrayOutputStream}
    6.18 -
    6.19 -import scala.io.{Source, BufferedSource}
    6.20 -
    6.21 -
    6.22 -object Isabelle_Encoding
    6.23 -{
    6.24 -  val NAME = "UTF-8-Isabelle"
    6.25 -
    6.26 -  def is_active(buffer: JEditBuffer): Boolean =
    6.27 -    buffer.getProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
    6.28 -}
    6.29 -
    6.30 -class Isabelle_Encoding extends Encoding
    6.31 -{
    6.32 -  private val charset = Charset.forName(Isabelle_System.charset)
    6.33 -  private val BUFSIZE = 32768
    6.34 -
    6.35 -  private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
    6.36 -  {
    6.37 -    def source(): Source =
    6.38 -      BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
    6.39 -    new CharArrayReader(Isabelle.symbols.decode(source.mkString).toArray)
    6.40 -  }
    6.41 -
    6.42 -	override def getTextReader(in: InputStream): Reader =
    6.43 -    text_reader(in, charset.newDecoder())
    6.44 -
    6.45 -	override def getPermissiveTextReader(in: InputStream): Reader =
    6.46 -	{
    6.47 -		val decoder = charset.newDecoder()
    6.48 -		decoder.onMalformedInput(CodingErrorAction.REPLACE)
    6.49 -		decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
    6.50 -		text_reader(in, decoder)
    6.51 -	}
    6.52 -
    6.53 -  override def getTextWriter(out: OutputStream): Writer =
    6.54 -  {
    6.55 -    val buffer = new ByteArrayOutputStream(BUFSIZE) {
    6.56 -      override def flush()
    6.57 -      {
    6.58 -        val text = Isabelle.symbols.encode(toString(Isabelle_System.charset))
    6.59 -        out.write(text.getBytes(Isabelle_System.charset))
    6.60 -        out.flush()
    6.61 -      }
    6.62 -      override def close() { out.close() }
    6.63 -    }
    6.64 -		new OutputStreamWriter(buffer, charset.newEncoder())
    6.65 -  }
    6.66 -}
     7.1 --- a/src/Tools/jEdit/src/jedit/OptionPane.scala	Tue Dec 08 14:29:29 2009 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,43 +0,0 @@
     7.4 -/*
     7.5 - * Editor pane for plugin options
     7.6 - *
     7.7 - * @author Johannes Hölzl, TU Munich
     7.8 - */
     7.9 -
    7.10 -package isabelle.jedit
    7.11 -
    7.12 -import javax.swing.{JComboBox, JSpinner}
    7.13 -
    7.14 -import org.gjt.sp.jedit.AbstractOptionPane
    7.15 -
    7.16 -
    7.17 -class OptionPane extends AbstractOptionPane("isabelle")
    7.18 -{
    7.19 -  private val logic_name = new JComboBox()
    7.20 -  private val font_size = new JSpinner()
    7.21 -
    7.22 -  override def _init()
    7.23 -  {
    7.24 -    addComponent(Isabelle.Property("logic.title"), {
    7.25 -      for (name <- Isabelle.system.find_logics()) {
    7.26 -        logic_name.addItem(name)
    7.27 -        if (name == Isabelle.Property("logic"))
    7.28 -          logic_name.setSelectedItem(name)
    7.29 -      }
    7.30 -      logic_name
    7.31 -    })
    7.32 -    addComponent(Isabelle.Property("font-size.title"), {
    7.33 -      font_size.setValue(Isabelle.Int_Property("font-size"))
    7.34 -      font_size
    7.35 -    })
    7.36 -  }
    7.37 -
    7.38 -  override def _save()
    7.39 -  {
    7.40 -    val logic = logic_name.getSelectedItem.asInstanceOf[String]
    7.41 -    Isabelle.Property("logic") = logic
    7.42 -
    7.43 -    val size = font_size.getValue().asInstanceOf[Int]
    7.44 -    Isabelle.Int_Property("font-size") = size
    7.45 -  }
    7.46 -}
     8.1 --- a/src/Tools/jEdit/src/jedit/OutputDockable.scala	Tue Dec 08 14:29:29 2009 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,31 +0,0 @@
     8.4 -/*
     8.5 - * Dockable window for raw process output
     8.6 - *
     8.7 - * @author Fabian Immler, TU Munich
     8.8 - * @author Johannes Hölzl, TU Munich
     8.9 - */
    8.10 -
    8.11 -package isabelle.jedit
    8.12 -
    8.13 -
    8.14 -import java.awt.{Dimension, Graphics, GridLayout}
    8.15 -import javax.swing.{JPanel, JTextArea, JScrollPane}
    8.16 -
    8.17 -import org.gjt.sp.jedit.View
    8.18 -import org.gjt.sp.jedit.gui.DockableWindowManager
    8.19 -
    8.20 -
    8.21 -class OutputDockable(view : View, position : String) extends JPanel {
    8.22 -
    8.23 -  if (position == DockableWindowManager.FLOATING)
    8.24 -    setPreferredSize(new Dimension(500, 250))
    8.25 -
    8.26 -  setLayout(new GridLayout(1, 1))
    8.27 -  add(new JScrollPane(new JTextArea))
    8.28 -
    8.29 -  def set_text(output_text_view: JTextArea) {
    8.30 -    removeAll()
    8.31 -    add(new JScrollPane(output_text_view))
    8.32 -    revalidate()
    8.33 -  }
    8.34 -}
     9.1 --- a/src/Tools/jEdit/src/jedit/Plugin.scala	Tue Dec 08 14:29:29 2009 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,155 +0,0 @@
     9.4 -/*
     9.5 - * Main Isabelle/jEdit plugin setup
     9.6 - *
     9.7 - * @author Johannes Hölzl, TU Munich
     9.8 - * @author Fabian Immler, TU Munich
     9.9 - */
    9.10 -
    9.11 -package isabelle.jedit
    9.12 -
    9.13 -
    9.14 -import java.io.{FileInputStream, IOException}
    9.15 -import java.awt.Font
    9.16 -import javax.swing.JScrollPane
    9.17 -
    9.18 -import scala.collection.mutable
    9.19 -
    9.20 -import isabelle.prover.{Prover, Command}
    9.21 -import isabelle.proofdocument.ProofDocument
    9.22 -import isabelle.Isabelle_System
    9.23 -
    9.24 -import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
    9.25 -import org.gjt.sp.jedit.buffer.JEditBuffer
    9.26 -import org.gjt.sp.jedit.textarea.JEditTextArea
    9.27 -import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
    9.28 -
    9.29 -
    9.30 -object Isabelle
    9.31 -{
    9.32 -  /* name */
    9.33 -
    9.34 -  val NAME = "Isabelle"
    9.35 -
    9.36 -
    9.37 -  /* properties */
    9.38 -
    9.39 -  val OPTION_PREFIX = "options.isabelle."
    9.40 -
    9.41 -  object Property
    9.42 -  {
    9.43 -    def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
    9.44 -    def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
    9.45 -  }
    9.46 -
    9.47 -  object Boolean_Property
    9.48 -  {
    9.49 -    def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
    9.50 -    def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
    9.51 -  }
    9.52 -
    9.53 -  object Int_Property
    9.54 -  {
    9.55 -    def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
    9.56 -    def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
    9.57 -  }
    9.58 -
    9.59 -
    9.60 -  /* Isabelle system instance */
    9.61 -
    9.62 -  var system: Isabelle_System = null
    9.63 -  def symbols = system.symbols
    9.64 -  lazy val completion = new Completion + symbols
    9.65 -
    9.66 -
    9.67 -  /* settings */
    9.68 -
    9.69 -  def default_logic(): String =
    9.70 -  {
    9.71 -    val logic = Isabelle.Property("logic")
    9.72 -    if (logic != null) logic
    9.73 -    else system.getenv_strict("ISABELLE_LOGIC")
    9.74 -  }
    9.75 -
    9.76 -
    9.77 -  /* plugin instance */
    9.78 -
    9.79 -  var plugin: Plugin = null
    9.80 -
    9.81 -
    9.82 -  /* running provers */
    9.83 -
    9.84 -  def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
    9.85 -}
    9.86 -
    9.87 -
    9.88 -class Plugin extends EBPlugin
    9.89 -{
    9.90 -  /* event buses */
    9.91 -
    9.92 -  val state_update = new Event_Bus[Command]
    9.93 -
    9.94 -
    9.95 -  /* selected state */
    9.96 -
    9.97 -  private var _selected_state: Command = null
    9.98 -  def selected_state = _selected_state
    9.99 -  def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
   9.100 -
   9.101 -
   9.102 -  /* mapping buffer <-> prover */
   9.103 -
   9.104 -  private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
   9.105 -
   9.106 -  private def install(view: View)
   9.107 -  {
   9.108 -    val buffer = view.getBuffer
   9.109 -    val prover_setup = new ProverSetup(buffer)
   9.110 -    mapping.update(buffer, prover_setup)
   9.111 -    prover_setup.activate(view)
   9.112 -  }
   9.113 -
   9.114 -  private def uninstall(view: View) =
   9.115 -    mapping.removeKey(view.getBuffer).get.deactivate
   9.116 -
   9.117 -  def switch_active (view: View) =
   9.118 -    if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
   9.119 -    else install(view)
   9.120 -
   9.121 -  def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
   9.122 -  def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
   9.123 -
   9.124 -
   9.125 -  /* main plugin plumbing */
   9.126 -
   9.127 -  override def handleMessage(msg: EBMessage)
   9.128 -  {
   9.129 -    msg match {
   9.130 -      case epu: EditPaneUpdate =>
   9.131 -        val buffer = epu.getEditPane.getBuffer
   9.132 -        epu.getWhat match {
   9.133 -          case EditPaneUpdate.BUFFER_CHANGED =>
   9.134 -            (mapping get buffer) map (_.theory_view.activate)
   9.135 -          case EditPaneUpdate.BUFFER_CHANGING =>
   9.136 -            if (buffer != null)
   9.137 -              (mapping get buffer) map (_.theory_view.deactivate)
   9.138 -          case _ =>
   9.139 -        }
   9.140 -      case _ =>
   9.141 -    }
   9.142 -  }
   9.143 -
   9.144 -  override def start()
   9.145 -  {
   9.146 -    Isabelle.plugin = this
   9.147 -    Isabelle.system = new Isabelle_System
   9.148 -    if (!Isabelle.system.register_fonts())
   9.149 -      System.err.println("Failed to register Isabelle fonts")
   9.150 -  }
   9.151 -
   9.152 -  override def stop()
   9.153 -  {
   9.154 -    // TODO: proper cleanup
   9.155 -    Isabelle.system = null
   9.156 -    Isabelle.plugin = null
   9.157 -  }
   9.158 -}
    10.1 --- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Tue Dec 08 14:29:29 2009 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,35 +0,0 @@
    10.4 -/*
    10.5 - * Independent prover sessions for each buffer
    10.6 - *
    10.7 - * @author Fabian Immler, TU Munich
    10.8 - */
    10.9 -
   10.10 -package isabelle.jedit
   10.11 -
   10.12 -
   10.13 -import org.gjt.sp.jedit.{Buffer, View}
   10.14 -
   10.15 -import isabelle.prover.Prover
   10.16 -
   10.17 -
   10.18 -class ProverSetup(buffer: Buffer)
   10.19 -{
   10.20 -  var prover: Prover = null
   10.21 -  var theory_view: TheoryView = null
   10.22 -
   10.23 -  def activate(view: View)
   10.24 -  {
   10.25 -    // TheoryView starts prover
   10.26 -    theory_view = new TheoryView(view.getTextArea)
   10.27 -    prover = theory_view.prover
   10.28 -
   10.29 -    theory_view.activate()
   10.30 -    prover.begin_document(buffer.getName)
   10.31 -  }
   10.32 -
   10.33 -  def deactivate()
   10.34 -  {
   10.35 -    theory_view.deactivate
   10.36 -    prover.stop
   10.37 -  }
   10.38 -}
    11.1 --- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Tue Dec 08 14:29:29 2009 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,111 +0,0 @@
    11.4 -/*
    11.5 - * Dockable window with rendered state output
    11.6 - *
    11.7 - * @author Fabian Immler, TU Munich
    11.8 - * @author Johannes Hölzl, TU Munich
    11.9 - */
   11.10 -
   11.11 -package isabelle.jedit
   11.12 -
   11.13 -import isabelle.XML
   11.14 -
   11.15 -import java.io.StringReader
   11.16 -import java.awt.{BorderLayout, Dimension}
   11.17 -
   11.18 -import javax.swing.{JButton, JPanel, JScrollPane}
   11.19 -
   11.20 -import java.util.logging.{Logger, Level}
   11.21 -
   11.22 -import org.lobobrowser.html.parser._
   11.23 -import org.lobobrowser.html.test._
   11.24 -import org.lobobrowser.html.gui._
   11.25 -import org.lobobrowser.html._
   11.26 -import org.lobobrowser.html.style.CSSUtilities
   11.27 -import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
   11.28 -
   11.29 -import org.gjt.sp.jedit.jEdit
   11.30 -import org.gjt.sp.jedit.View
   11.31 -import org.gjt.sp.jedit.gui.DockableWindowManager
   11.32 -import org.gjt.sp.jedit.textarea.AntiAlias
   11.33 -
   11.34 -import scala.io.Source
   11.35 -
   11.36 -
   11.37 -class StateViewDockable(view : View, position : String) extends JPanel {
   11.38 -
   11.39 -  // outer panel
   11.40 -  if (position == DockableWindowManager.FLOATING)
   11.41 -    setPreferredSize(new Dimension(500, 250))
   11.42 -  setLayout(new BorderLayout)
   11.43 -
   11.44 -
   11.45 -  // global logging
   11.46 -  
   11.47 -  Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
   11.48 -
   11.49 -
   11.50 -  // document template with styles
   11.51 -
   11.52 -  private def try_file(name: String): String =
   11.53 -  {
   11.54 -    val file = Isabelle.system.platform_file(name)
   11.55 -    if (file.exists) Source.fromFile(file).mkString else ""
   11.56 -  }
   11.57 -
   11.58 -
   11.59 -  // HTML panel
   11.60 -
   11.61 -  val panel = new HtmlPanel
   11.62 -  val ucontext = new SimpleUserAgentContext
   11.63 -  val rcontext = new SimpleHtmlRendererContext(panel, ucontext)
   11.64 -  val doc = {
   11.65 -    val builder = new DocumentBuilderImpl(ucontext, rcontext)
   11.66 -    builder.parse(new InputSourceImpl(new StringReader(
   11.67 -      """<?xml version="1.0" encoding="utf-8"?>
   11.68 -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
   11.69 -  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
   11.70 -<html xmlns="http://www.w3.org/1999/xhtml">
   11.71 -<head>
   11.72 -<style media="all" type="text/css">
   11.73 -""" +
   11.74 -  try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
   11.75 -"""
   11.76 -body {
   11.77 -  font-family: IsabelleText;
   11.78 -  font-size: 14pt;
   11.79 -}
   11.80 -""" +
   11.81 -  try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
   11.82 -"""
   11.83 -</style>
   11.84 -</head>
   11.85 -</html>
   11.86 -""")))
   11.87 -  }
   11.88 -
   11.89 -  val empty_body = XML.document_node(doc, XML.elem(HTML.BODY))
   11.90 -  doc.appendChild(empty_body)
   11.91 -
   11.92 -  panel.setDocument(doc, rcontext)
   11.93 -  add(panel, BorderLayout.CENTER)
   11.94 -
   11.95 -  
   11.96 -  // register for state-view
   11.97 -  Isabelle.plugin.state_update += (cmd => {
   11.98 -    val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
   11.99 -
  11.100 -    Swing_Thread.later {
  11.101 -      val node =
  11.102 -        if (cmd == null) empty_body
  11.103 -        else {
  11.104 -          val xml = XML.elem(HTML.BODY,
  11.105 -            cmd.results(theory_view.current_document).
  11.106 -              map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t))))
  11.107 -          XML.document_node(doc, xml)
  11.108 -        }
  11.109 -      doc.removeChild(doc.getLastChild())
  11.110 -      doc.appendChild(node)
  11.111 -      panel.delayedRelayout(node.asInstanceOf[NodeImpl])
  11.112 -    }
  11.113 -  })
  11.114 -}
    12.1 --- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Dec 08 14:29:29 2009 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,327 +0,0 @@
    12.4 -/*
    12.5 - * jEdit text area as document text source
    12.6 - *
    12.7 - * @author Fabian Immler, TU Munich
    12.8 - * @author Johannes Hölzl, TU Munich
    12.9 - * @author Makarius
   12.10 - */
   12.11 -
   12.12 -package isabelle.jedit
   12.13 -
   12.14 -import scala.actors.Actor, Actor._
   12.15 -import scala.collection.mutable
   12.16 -
   12.17 -import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove}
   12.18 -import isabelle.prover.{Prover, Command}
   12.19 -
   12.20 -import java.awt.{Color, Graphics2D}
   12.21 -import javax.swing.event.{CaretListener, CaretEvent}
   12.22 -
   12.23 -import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
   12.24 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
   12.25 -import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
   12.26 -
   12.27 -
   12.28 -object TheoryView
   12.29 -{
   12.30 -  def choose_color(command: Command, doc: ProofDocument): Color =
   12.31 -  {
   12.32 -    command.status(doc) match {
   12.33 -      case Command.Status.UNPROCESSED => new Color(255, 228, 225)
   12.34 -      case Command.Status.FINISHED => new Color(234, 248, 255)
   12.35 -      case Command.Status.FAILED => new Color(255, 106, 106)
   12.36 -      case _ => Color.red
   12.37 -    }
   12.38 -  }
   12.39 -}
   12.40 -
   12.41 -
   12.42 -class TheoryView(text_area: JEditTextArea)
   12.43 -{
   12.44 -  private val buffer = text_area.getBuffer
   12.45 -
   12.46 -
   12.47 -  /* prover setup */
   12.48 -
   12.49 -  val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic())
   12.50 -
   12.51 -  prover.command_change += ((command: Command) =>
   12.52 -    if (current_document().commands.contains(command))
   12.53 -      Swing_Thread.later {
   12.54 -        // FIXME proper handling of buffer vs. text areas
   12.55 -        // repaint if buffer is active
   12.56 -        if (text_area.getBuffer == buffer) {
   12.57 -          update_syntax(command)
   12.58 -          invalidate_line(command)
   12.59 -          overview.repaint()
   12.60 -        }
   12.61 -      })
   12.62 -
   12.63 -
   12.64 -  /* changes vs. edits */
   12.65 -
   12.66 -  private val change_0 = new Change(prover.document_0.id, None, Nil)
   12.67 -  private var _changes = List(change_0)   // owned by Swing/AWT thread
   12.68 -  def changes = _changes
   12.69 -  private var current_change = change_0
   12.70 -
   12.71 -  private val edits = new mutable.ListBuffer[Edit]   // owned by Swing thread
   12.72 -
   12.73 -  private val edits_delay = Swing_Thread.delay_last(300) {
   12.74 -    if (!edits.isEmpty) {
   12.75 -      val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList)
   12.76 -      _changes ::= change
   12.77 -      prover.input(change)
   12.78 -      current_change = change
   12.79 -      edits.clear
   12.80 -    }
   12.81 -  }
   12.82 -
   12.83 -
   12.84 -  /* buffer_listener */
   12.85 -
   12.86 -  private val buffer_listener = new BufferListener {
   12.87 -    override def preContentInserted(buffer: JEditBuffer,
   12.88 -      start_line: Int, offset: Int, num_lines: Int, length: Int)
   12.89 -    {
   12.90 -      edits += Insert(offset, buffer.getText(offset, length))
   12.91 -      edits_delay()
   12.92 -    }
   12.93 -
   12.94 -    override def preContentRemoved(buffer: JEditBuffer,
   12.95 -      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
   12.96 -    {
   12.97 -      edits += Remove(start, buffer.getText(start, removed_length))
   12.98 -      edits_delay()
   12.99 -    }
  12.100 -
  12.101 -    override def contentInserted(buffer: JEditBuffer,
  12.102 -      start_line: Int, offset: Int, num_lines: Int, length: Int) { }
  12.103 -
  12.104 -    override def contentRemoved(buffer: JEditBuffer,
  12.105 -      start_line: Int, offset: Int, num_lines: Int, length: Int) { }
  12.106 -
  12.107 -    override def bufferLoaded(buffer: JEditBuffer) { }
  12.108 -    override def foldHandlerChanged(buffer: JEditBuffer) { }
  12.109 -    override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
  12.110 -    override def transactionComplete(buffer: JEditBuffer) { }
  12.111 -  }
  12.112 -
  12.113 -
  12.114 -  /* text_area_extension */
  12.115 -
  12.116 -  private val text_area_extension = new TextAreaExtension {
  12.117 -    override def paintValidLine(gfx: Graphics2D,
  12.118 -      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
  12.119 -    {
  12.120 -      val document = current_document()
  12.121 -      def from_current(pos: Int) = TheoryView.this.from_current(document, pos)
  12.122 -      def to_current(pos: Int) = TheoryView.this.to_current(document, pos)
  12.123 -      val saved_color = gfx.getColor
  12.124 -
  12.125 -      val metrics = text_area.getPainter.getFontMetrics
  12.126 -
  12.127 -      // encolor phase
  12.128 -      var cmd = document.command_at(from_current(start))
  12.129 -      while (cmd.isDefined && cmd.get.start(document) < end) {
  12.130 -        val e = cmd.get
  12.131 -        val begin = start max to_current(e.start(document))
  12.132 -        val finish = (end - 1) min to_current(e.stop(document))
  12.133 -        encolor(gfx, y, metrics.getHeight, begin, finish,
  12.134 -          TheoryView.choose_color(e, document), true)
  12.135 -        cmd = document.commands.next(e)
  12.136 -      }
  12.137 -
  12.138 -      gfx.setColor(saved_color)
  12.139 -    }
  12.140 -
  12.141 -    override def getToolTipText(x: Int, y: Int): String =
  12.142 -    {
  12.143 -      val document = current_document()
  12.144 -      val offset = from_current(document, text_area.xyToOffset(x, y))
  12.145 -      document.command_at(offset) match {
  12.146 -        case Some(cmd) =>
  12.147 -          document.token_start(cmd.tokens.first)
  12.148 -          cmd.type_at(document, offset - cmd.start(document)).getOrElse(null)
  12.149 -        case None => null
  12.150 -      }
  12.151 -    }
  12.152 -  }
  12.153 -
  12.154 -
  12.155 -  /* activation */
  12.156 -
  12.157 -  private val overview = new Document_Overview(prover, text_area, to_current)
  12.158 -
  12.159 -  private val selected_state_controller = new CaretListener {
  12.160 -    override def caretUpdate(e: CaretEvent) {
  12.161 -      val doc = current_document()
  12.162 -      doc.command_at(e.getDot) match {
  12.163 -        case Some(cmd)
  12.164 -          if (doc.token_start(cmd.tokens.first) <= e.getDot &&
  12.165 -            Isabelle.plugin.selected_state != cmd) =>
  12.166 -          Isabelle.plugin.selected_state = cmd
  12.167 -        case _ =>
  12.168 -      }
  12.169 -    }
  12.170 -  }
  12.171 -
  12.172 -  def activate() {
  12.173 -    text_area.addCaretListener(selected_state_controller)
  12.174 -    text_area.addLeftOfScrollBar(overview)
  12.175 -    text_area.getPainter.
  12.176 -      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
  12.177 -    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
  12.178 -    buffer.addBufferListener(buffer_listener)
  12.179 -
  12.180 -    val dockable =
  12.181 -      text_area.getView.getDockableWindowManager.getDockable("isabelle-output")
  12.182 -    if (dockable != null) {
  12.183 -      val output_dockable = dockable.asInstanceOf[OutputDockable]
  12.184 -      val output_text_view = prover.output_text_view
  12.185 -      output_dockable.set_text(output_text_view)
  12.186 -    }
  12.187 -
  12.188 -    buffer.propertiesChanged()
  12.189 -  }
  12.190 -
  12.191 -  def deactivate() {
  12.192 -    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
  12.193 -    buffer.removeBufferListener(buffer_listener)
  12.194 -    text_area.getPainter.removeExtension(text_area_extension)
  12.195 -    text_area.removeLeftOfScrollBar(overview)
  12.196 -    text_area.removeCaretListener(selected_state_controller)
  12.197 -  }
  12.198 -
  12.199 -
  12.200 -  /* history of changes */
  12.201 -
  12.202 -  private def doc_or_pred(c: Change): ProofDocument =
  12.203 -    prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
  12.204 -
  12.205 -  def current_document() = doc_or_pred(current_change)
  12.206 -
  12.207 -
  12.208 -  /* update to desired version */
  12.209 -
  12.210 -  def set_version(goal: Change) {
  12.211 -    // changes in buffer must be ignored
  12.212 -    buffer.removeBufferListener(buffer_listener)
  12.213 -
  12.214 -    def apply(change: Change): Unit = change.edits.foreach {
  12.215 -      case Insert(start, text) => buffer.insert(start, text)
  12.216 -      case Remove(start, text) => buffer.remove(start, text.length)
  12.217 -    }
  12.218 -
  12.219 -    def unapply(change: Change): Unit = change.edits.reverse.foreach {
  12.220 -      case Insert(start, text) => buffer.remove(start, text.length)
  12.221 -      case Remove(start, text) => buffer.insert(start, text)
  12.222 -    }
  12.223 -
  12.224 -    // undo/redo changes
  12.225 -    val ancs_current = current_change.ancestors
  12.226 -    val ancs_goal = goal.ancestors
  12.227 -    val paired = ancs_current.reverse zip ancs_goal.reverse
  12.228 -    def last_common[A](xs: List[(A, A)]): Option[A] = {
  12.229 -      xs match {
  12.230 -        case (x, y) :: xs =>
  12.231 -          if (x == y)
  12.232 -            xs match {
  12.233 -              case (a, b) :: ys =>
  12.234 -                if (a == b) last_common(xs)
  12.235 -                else Some(x)
  12.236 -              case _ => Some(x)
  12.237 -            }
  12.238 -          else None
  12.239 -        case _ => None
  12.240 -      }
  12.241 -    }
  12.242 -    val common_anc = last_common(paired).get
  12.243 -
  12.244 -    ancs_current.takeWhile(_ != common_anc) map unapply
  12.245 -    ancs_goal.takeWhile(_ != common_anc).reverse map apply
  12.246 -
  12.247 -    current_change = goal
  12.248 -    // invoke repaint
  12.249 -    buffer.propertiesChanged()
  12.250 -    invalidate_all()
  12.251 -    overview.repaint()
  12.252 -
  12.253 -    // track changes in buffer
  12.254 -    buffer.addBufferListener(buffer_listener)
  12.255 -  }
  12.256 -
  12.257 -
  12.258 -  /* transforming offsets */
  12.259 -
  12.260 -  private def changes_from(doc: ProofDocument): List[Edit] =
  12.261 -    List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
  12.262 -      edits.toList
  12.263 -
  12.264 -  def from_current(doc: ProofDocument, offset: Int): Int =
  12.265 -    (offset /: changes_from(doc).reverse) ((i, change) => change before i)
  12.266 -
  12.267 -  def to_current(doc: ProofDocument, offset: Int): Int =
  12.268 -    (offset /: changes_from(doc)) ((i, change) => change after i)
  12.269 -
  12.270 -
  12.271 -  private def lines_of_command(cmd: Command) =
  12.272 -  {
  12.273 -    val document = current_document()
  12.274 -    (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
  12.275 -     buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
  12.276 -  }
  12.277 -
  12.278 -
  12.279 -  /* (re)painting */
  12.280 -
  12.281 -  private val update_delay = Swing_Thread.delay_first(500) { buffer.propertiesChanged() }
  12.282 -
  12.283 -  private def update_syntax(cmd: Command) {
  12.284 -    val (line1, line2) = lines_of_command(cmd)
  12.285 -    if (line2 >= text_area.getFirstLine &&
  12.286 -      line1 <= text_area.getFirstLine + text_area.getVisibleLines)
  12.287 -        update_delay()
  12.288 -  }
  12.289 -
  12.290 -  private def invalidate_line(cmd: Command) =
  12.291 -  {
  12.292 -    val (start, stop) = lines_of_command(cmd)
  12.293 -    text_area.invalidateLineRange(start, stop)
  12.294 -
  12.295 -    if (Isabelle.plugin.selected_state == cmd)
  12.296 -      Isabelle.plugin.selected_state = cmd  // update State view
  12.297 -  }
  12.298 -
  12.299 -  private def invalidate_all() =
  12.300 -    text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
  12.301 -      text_area.getLastPhysicalLine)
  12.302 -
  12.303 -  private def encolor(gfx: Graphics2D,
  12.304 -    y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
  12.305 -  {
  12.306 -    val start = text_area.offsetToXY(begin)
  12.307 -    val stop =
  12.308 -      if (finish < buffer.getLength) text_area.offsetToXY(finish)
  12.309 -      else {
  12.310 -        val p = text_area.offsetToXY(finish - 1)
  12.311 -        val metrics = text_area.getPainter.getFontMetrics
  12.312 -        p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
  12.313 -        p
  12.314 -      }
  12.315 -
  12.316 -    if (start != null && stop != null) {
  12.317 -      gfx.setColor(color)
  12.318 -      if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
  12.319 -      else gfx.drawRect(start.x, y, stop.x - start.x, height)
  12.320 -    }
  12.321 -  }
  12.322 -
  12.323 -
  12.324 -  /* init */
  12.325 -
  12.326 -  prover.start()
  12.327 -
  12.328 -  edits += Insert(0, buffer.getText(0, buffer.getLength))
  12.329 -  edits_delay()
  12.330 -}
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Tools/jEdit/src/jedit/browse_version_dockable.scala	Tue Dec 08 14:49:01 2009 +0100
    13.3 @@ -0,0 +1,43 @@
    13.4 +/*
    13.5 + * Dockable window for navigating through the document-versions
    13.6 + *
    13.7 + * @author Fabian Immler, TU Munich
    13.8 + */
    13.9 +
   13.10 +package isabelle.jedit
   13.11 +
   13.12 +import isabelle.proofdocument.Change
   13.13 +
   13.14 +import java.awt.Dimension
   13.15 +import scala.swing.{ListView, FlowPanel}
   13.16 +import scala.swing.event.ListSelectionChanged
   13.17 +
   13.18 +import org.gjt.sp.jedit.View
   13.19 +import org.gjt.sp.jedit.gui.DockableWindowManager
   13.20 +
   13.21 +
   13.22 +class BrowseVersionDockable(view: View, position: String) extends FlowPanel
   13.23 +{
   13.24 +  if (position == DockableWindowManager.FLOATING)
   13.25 +    preferredSize = new Dimension(500, 250)
   13.26 +
   13.27 +  def prover_setup(): Option[ProverSetup] = Isabelle.prover_setup(view.getBuffer)
   13.28 +  def get_versions() =
   13.29 +    prover_setup() match {
   13.30 +      case None => Nil
   13.31 +      case Some(setup) => setup.theory_view.changes
   13.32 +    }
   13.33 +
   13.34 +  val list = new ListView[Change]
   13.35 +  list.fixedCellWidth = 500
   13.36 +  list.listData = get_versions()
   13.37 +  contents += list
   13.38 +
   13.39 +  listenTo(list.selection)
   13.40 +  reactions += {
   13.41 +    case ListSelectionChanged(source, range, false) =>
   13.42 +        prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
   13.43 +    }
   13.44 +
   13.45 +  prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
   13.46 +}
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Tools/jEdit/src/jedit/document_overview.scala	Tue Dec 08 14:49:01 2009 +0100
    14.3 @@ -0,0 +1,82 @@
    14.4 +/*
    14.5 + * Information on command status left of scrollbar (with panel)
    14.6 + *
    14.7 + * @author Fabian Immler, TU Munich
    14.8 + */
    14.9 +
   14.10 +package isabelle.jedit
   14.11 +
   14.12 +import isabelle.prover.{Prover, Command}
   14.13 +import isabelle.proofdocument.ProofDocument
   14.14 +
   14.15 +import javax.swing.{JPanel, ToolTipManager}
   14.16 +import java.awt.event.{MouseAdapter, MouseEvent}
   14.17 +import java.awt.{BorderLayout, Graphics, Dimension}
   14.18 +
   14.19 +import org.gjt.sp.jedit.gui.RolloverButton
   14.20 +import org.gjt.sp.jedit.textarea.JEditTextArea
   14.21 +import org.gjt.sp.jedit.buffer.JEditBuffer
   14.22 +
   14.23 +
   14.24 +class Document_Overview(
   14.25 +    prover: Prover,
   14.26 +    text_area: JEditTextArea,
   14.27 +    to_current: (ProofDocument, Int) => Int)
   14.28 +  extends JPanel(new BorderLayout)
   14.29 +{
   14.30 +  private val WIDTH = 10
   14.31 +  private val HEIGHT = 2
   14.32 +
   14.33 +  setRequestFocusEnabled(false)
   14.34 +
   14.35 +  addMouseListener(new MouseAdapter {
   14.36 +    override def mousePressed(event: MouseEvent) {
   14.37 +      val line = y_to_line(event.getY)
   14.38 +      if (line >= 0 && line < text_area.getLineCount)
   14.39 +        text_area.setCaretPosition(text_area.getLineStartOffset(line))
   14.40 +    }
   14.41 +  })
   14.42 +
   14.43 +  override def addNotify() {
   14.44 +    super.addNotify()
   14.45 +    ToolTipManager.sharedInstance.registerComponent(this)
   14.46 +  }
   14.47 +
   14.48 +  override def removeNotify() {
   14.49 +    super.removeNotify
   14.50 +    ToolTipManager.sharedInstance.unregisterComponent(this)
   14.51 +  }
   14.52 +
   14.53 +  override def getToolTipText(event: MouseEvent): String =
   14.54 +  {
   14.55 +    val buffer = text_area.getBuffer
   14.56 +    val lineCount = buffer.getLineCount
   14.57 +    val line = y_to_line(event.getY())
   14.58 +    if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
   14.59 +    else ""
   14.60 +  }
   14.61 +
   14.62 +  override def paintComponent(gfx: Graphics) {
   14.63 +    super.paintComponent(gfx)
   14.64 +    val buffer = text_area.getBuffer
   14.65 +    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
   14.66 +    val doc = theory_view.current_document()
   14.67 +
   14.68 +    for (command <- doc.commands) {
   14.69 +      val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc)))
   14.70 +      val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1
   14.71 +      val y = line_to_y(line1)
   14.72 +      val height = HEIGHT * (line2 - line1)
   14.73 +      gfx.setColor(TheoryView.choose_color(command, doc))
   14.74 +      gfx.fillRect(0, y, getWidth - 1, height)
   14.75 +    }
   14.76 +  }
   14.77 +
   14.78 +  override def getPreferredSize = new Dimension(WIDTH, 0)
   14.79 +
   14.80 +  private def line_to_y(line: Int): Int =
   14.81 +    (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
   14.82 +
   14.83 +  private def y_to_line(y: Int): Int =
   14.84 +    (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
   14.85 +}
   14.86 \ No newline at end of file
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala	Tue Dec 08 14:49:01 2009 +0100
    15.3 @@ -0,0 +1,63 @@
    15.4 +/*
    15.5 + * Isabelle encoding -- based on utf-8
    15.6 + *
    15.7 + * @author Makarius
    15.8 + */
    15.9 +
   15.10 +package isabelle.jedit
   15.11 +
   15.12 +import org.gjt.sp.jedit.io.Encoding
   15.13 +import org.gjt.sp.jedit.buffer.JEditBuffer
   15.14 +
   15.15 +import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
   15.16 +import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
   15.17 +  CharArrayReader, ByteArrayOutputStream}
   15.18 +
   15.19 +import scala.io.{Source, BufferedSource}
   15.20 +
   15.21 +
   15.22 +object Isabelle_Encoding
   15.23 +{
   15.24 +  val NAME = "UTF-8-Isabelle"
   15.25 +
   15.26 +  def is_active(buffer: JEditBuffer): Boolean =
   15.27 +    buffer.getProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
   15.28 +}
   15.29 +
   15.30 +class Isabelle_Encoding extends Encoding
   15.31 +{
   15.32 +  private val charset = Charset.forName(Isabelle_System.charset)
   15.33 +  private val BUFSIZE = 32768
   15.34 +
   15.35 +  private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
   15.36 +  {
   15.37 +    def source(): Source =
   15.38 +      BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
   15.39 +    new CharArrayReader(Isabelle.symbols.decode(source.mkString).toArray)
   15.40 +  }
   15.41 +
   15.42 +	override def getTextReader(in: InputStream): Reader =
   15.43 +    text_reader(in, charset.newDecoder())
   15.44 +
   15.45 +	override def getPermissiveTextReader(in: InputStream): Reader =
   15.46 +	{
   15.47 +		val decoder = charset.newDecoder()
   15.48 +		decoder.onMalformedInput(CodingErrorAction.REPLACE)
   15.49 +		decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
   15.50 +		text_reader(in, decoder)
   15.51 +	}
   15.52 +
   15.53 +  override def getTextWriter(out: OutputStream): Writer =
   15.54 +  {
   15.55 +    val buffer = new ByteArrayOutputStream(BUFSIZE) {
   15.56 +      override def flush()
   15.57 +      {
   15.58 +        val text = Isabelle.symbols.encode(toString(Isabelle_System.charset))
   15.59 +        out.write(text.getBytes(Isabelle_System.charset))
   15.60 +        out.flush()
   15.61 +      }
   15.62 +      override def close() { out.close() }
   15.63 +    }
   15.64 +		new OutputStreamWriter(buffer, charset.newEncoder())
   15.65 +  }
   15.66 +}
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Dec 08 14:49:01 2009 +0100
    16.3 @@ -0,0 +1,80 @@
    16.4 +/*
    16.5 + * Hyperlink setup for Isabelle proof documents
    16.6 + *
    16.7 + * @author Fabian Immler, TU Munich
    16.8 + */
    16.9 +
   16.10 +package isabelle.jedit
   16.11 +
   16.12 +import java.io.File
   16.13 +
   16.14 +import gatchan.jedit.hyperlinks.Hyperlink
   16.15 +import gatchan.jedit.hyperlinks.HyperlinkSource
   16.16 +import gatchan.jedit.hyperlinks.AbstractHyperlink
   16.17 +
   16.18 +import org.gjt.sp.jedit.View
   16.19 +import org.gjt.sp.jedit.jEdit
   16.20 +import org.gjt.sp.jedit.Buffer
   16.21 +import org.gjt.sp.jedit.TextUtilities
   16.22 +
   16.23 +import isabelle.prover.Command
   16.24 +
   16.25 +
   16.26 +class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
   16.27 +  extends AbstractHyperlink(start, end, line, "")
   16.28 +{
   16.29 +  override def click(view: View) {
   16.30 +    view.getTextArea.moveCaretPosition(ref_offset)
   16.31 +  }
   16.32 +}
   16.33 +
   16.34 +class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
   16.35 +  extends AbstractHyperlink(start, end, line, "")
   16.36 +{
   16.37 +  override def click(view: View) = {
   16.38 +    Isabelle.system.source_file(ref_file) match {
   16.39 +      case None => System.err.println("Could not find source file " + ref_file)
   16.40 +      case Some(file) =>
   16.41 +        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
   16.42 +    }
   16.43 +  }
   16.44 +}
   16.45 +
   16.46 +class IsabelleHyperlinkSource extends HyperlinkSource
   16.47 +{
   16.48 +	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
   16.49 +    val prover = Isabelle.prover_setup(buffer).map(_.prover)
   16.50 +    val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
   16.51 +    if (prover.isEmpty || theory_view_opt.isEmpty) null
   16.52 +    else if (prover.get == null || theory_view_opt.get == null) null
   16.53 +    else {
   16.54 +      val theory_view = theory_view_opt.get
   16.55 +      val document = theory_view.current_document()
   16.56 +      val offset = theory_view.from_current(document, original_offset)
   16.57 +      document.command_at(offset) match {
   16.58 +        case Some(command) =>
   16.59 +          command.ref_at(document, offset - command.start(document)) match {
   16.60 +            case Some(ref) =>
   16.61 +              val command_start = command.start(document)
   16.62 +              val begin = theory_view.to_current(document, command_start + ref.start)
   16.63 +              val line = buffer.getLineOfOffset(begin)
   16.64 +              val end = theory_view.to_current(document, command_start + ref.stop)
   16.65 +              ref.info match {
   16.66 +                case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
   16.67 +                  new ExternalHyperlink(begin, end, line, ref_file, ref_line)
   16.68 +                case Command.RefInfo(_, _, Some(id), Some(offset)) =>
   16.69 +                  prover.get.command(id) match {
   16.70 +                    case Some(ref_cmd) =>
   16.71 +                      new InternalHyperlink(begin, end, line,
   16.72 +                        theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
   16.73 +                    case None => null
   16.74 +                  }
   16.75 +                case _ => null
   16.76 +              }
   16.77 +            case None => null
   16.78 +          }
   16.79 +        case None => null
   16.80 +      }
   16.81 +    }
   16.82 +  }
   16.83 +}
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Dec 08 14:49:01 2009 +0100
    17.3 @@ -0,0 +1,102 @@
    17.4 +/*
    17.5 + * SideKick parser for Isabelle proof documents
    17.6 + *
    17.7 + * @author Fabian Immler, TU Munich
    17.8 + * @author Makarius
    17.9 + */
   17.10 +
   17.11 +package isabelle.jedit
   17.12 +
   17.13 +import scala.collection.Set
   17.14 +import scala.collection.immutable.TreeSet
   17.15 +
   17.16 +import javax.swing.tree.DefaultMutableTreeNode
   17.17 +import javax.swing.text.Position
   17.18 +import javax.swing.Icon
   17.19 +
   17.20 +import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
   17.21 +import errorlist.DefaultErrorSource
   17.22 +import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
   17.23 +
   17.24 +import isabelle.prover.{Command, Markup_Node}
   17.25 +import isabelle.proofdocument.ProofDocument
   17.26 +
   17.27 +
   17.28 +class IsabelleSideKickParser extends SideKickParser("isabelle")
   17.29 +{
   17.30 +  /* parsing */
   17.31 +
   17.32 +  @volatile private var stopped = false
   17.33 +  override def stop() = { stopped = true }
   17.34 +
   17.35 +  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
   17.36 +  {
   17.37 +    implicit def int_to_pos(offset: Int): Position =
   17.38 +      new Position { def getOffset = offset; override def toString = offset.toString }
   17.39 +
   17.40 +    stopped = false
   17.41 +
   17.42 +    val data = new SideKickParsedData(buffer.getName)
   17.43 +    val root = data.root
   17.44 +    data.getAsset(root).setEnd(buffer.getLength)
   17.45 +
   17.46 +    val prover_setup = Isabelle.prover_setup(buffer)
   17.47 +    if (prover_setup.isDefined) {
   17.48 +      val document = prover_setup.get.theory_view.current_document()
   17.49 +      for (command <- document.commands if !stopped) {
   17.50 +        root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
   17.51 +            {
   17.52 +              val content = command.content(node.start, node.stop)
   17.53 +              val command_start = command.start(document)
   17.54 +              val id = command.id
   17.55 +
   17.56 +              new DefaultMutableTreeNode(new IAsset {
   17.57 +                override def getIcon: Icon = null
   17.58 +                override def getShortString: String = content
   17.59 +                override def getLongString: String = node.info.toString
   17.60 +                override def getName: String = id
   17.61 +                override def setName(name: String) = ()
   17.62 +                override def setStart(start: Position) = ()
   17.63 +                override def getStart: Position = command_start + node.start
   17.64 +                override def setEnd(end: Position) = ()
   17.65 +                override def getEnd: Position = command_start + node.stop
   17.66 +                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
   17.67 +              })
   17.68 +            }))
   17.69 +      }
   17.70 +      if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
   17.71 +    }
   17.72 +    else root.add(new DefaultMutableTreeNode("<buffer inactive>"))
   17.73 +
   17.74 +    data
   17.75 +  }
   17.76 +
   17.77 +
   17.78 +  /* completion */
   17.79 +
   17.80 +  override def supportsCompletion = true
   17.81 +  override def canCompleteAnywhere = true
   17.82 +
   17.83 +  override def complete(pane: EditPane, caret: Int): SideKickCompletion =
   17.84 +  {
   17.85 +    val buffer = pane.getBuffer
   17.86 +
   17.87 +    val line = buffer.getLineOfOffset(caret)
   17.88 +    val start = buffer.getLineStartOffset(line)
   17.89 +    val text = buffer.getSegment(start, caret - start)
   17.90 +
   17.91 +    val completion =
   17.92 +      Isabelle.prover_setup(buffer).map(_.prover.completion()).getOrElse(Isabelle.completion)
   17.93 +
   17.94 +    completion.complete(text) match {
   17.95 +      case None => null
   17.96 +      case Some((word, cs)) =>
   17.97 +        val ds =
   17.98 +          if (Isabelle_Encoding.is_active(buffer))
   17.99 +            cs.map(Isabelle.system.symbols.decode(_)).sort(Completion.length_ord _)
  17.100 +          else cs
  17.101 +        new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
  17.102 +    }
  17.103 +  }
  17.104 +
  17.105 +}
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/Tools/jEdit/src/jedit/option_pane.scala	Tue Dec 08 14:49:01 2009 +0100
    18.3 @@ -0,0 +1,43 @@
    18.4 +/*
    18.5 + * Editor pane for plugin options
    18.6 + *
    18.7 + * @author Johannes Hölzl, TU Munich
    18.8 + */
    18.9 +
   18.10 +package isabelle.jedit
   18.11 +
   18.12 +import javax.swing.{JComboBox, JSpinner}
   18.13 +
   18.14 +import org.gjt.sp.jedit.AbstractOptionPane
   18.15 +
   18.16 +
   18.17 +class OptionPane extends AbstractOptionPane("isabelle")
   18.18 +{
   18.19 +  private val logic_name = new JComboBox()
   18.20 +  private val font_size = new JSpinner()
   18.21 +
   18.22 +  override def _init()
   18.23 +  {
   18.24 +    addComponent(Isabelle.Property("logic.title"), {
   18.25 +      for (name <- Isabelle.system.find_logics()) {
   18.26 +        logic_name.addItem(name)
   18.27 +        if (name == Isabelle.Property("logic"))
   18.28 +          logic_name.setSelectedItem(name)
   18.29 +      }
   18.30 +      logic_name
   18.31 +    })
   18.32 +    addComponent(Isabelle.Property("font-size.title"), {
   18.33 +      font_size.setValue(Isabelle.Int_Property("font-size"))
   18.34 +      font_size
   18.35 +    })
   18.36 +  }
   18.37 +
   18.38 +  override def _save()
   18.39 +  {
   18.40 +    val logic = logic_name.getSelectedItem.asInstanceOf[String]
   18.41 +    Isabelle.Property("logic") = logic
   18.42 +
   18.43 +    val size = font_size.getValue().asInstanceOf[Int]
   18.44 +    Isabelle.Int_Property("font-size") = size
   18.45 +  }
   18.46 +}
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 14:49:01 2009 +0100
    19.3 @@ -0,0 +1,155 @@
    19.4 +/*
    19.5 + * Main Isabelle/jEdit plugin setup
    19.6 + *
    19.7 + * @author Johannes Hölzl, TU Munich
    19.8 + * @author Fabian Immler, TU Munich
    19.9 + */
   19.10 +
   19.11 +package isabelle.jedit
   19.12 +
   19.13 +
   19.14 +import java.io.{FileInputStream, IOException}
   19.15 +import java.awt.Font
   19.16 +import javax.swing.JScrollPane
   19.17 +
   19.18 +import scala.collection.mutable
   19.19 +
   19.20 +import isabelle.prover.{Prover, Command}
   19.21 +import isabelle.proofdocument.ProofDocument
   19.22 +import isabelle.Isabelle_System
   19.23 +
   19.24 +import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
   19.25 +import org.gjt.sp.jedit.buffer.JEditBuffer
   19.26 +import org.gjt.sp.jedit.textarea.JEditTextArea
   19.27 +import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
   19.28 +
   19.29 +
   19.30 +object Isabelle
   19.31 +{
   19.32 +  /* name */
   19.33 +
   19.34 +  val NAME = "Isabelle"
   19.35 +
   19.36 +
   19.37 +  /* properties */
   19.38 +
   19.39 +  val OPTION_PREFIX = "options.isabelle."
   19.40 +
   19.41 +  object Property
   19.42 +  {
   19.43 +    def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
   19.44 +    def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
   19.45 +  }
   19.46 +
   19.47 +  object Boolean_Property
   19.48 +  {
   19.49 +    def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
   19.50 +    def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
   19.51 +  }
   19.52 +
   19.53 +  object Int_Property
   19.54 +  {
   19.55 +    def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
   19.56 +    def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
   19.57 +  }
   19.58 +
   19.59 +
   19.60 +  /* Isabelle system instance */
   19.61 +
   19.62 +  var system: Isabelle_System = null
   19.63 +  def symbols = system.symbols
   19.64 +  lazy val completion = new Completion + symbols
   19.65 +
   19.66 +
   19.67 +  /* settings */
   19.68 +
   19.69 +  def default_logic(): String =
   19.70 +  {
   19.71 +    val logic = Isabelle.Property("logic")
   19.72 +    if (logic != null) logic
   19.73 +    else system.getenv_strict("ISABELLE_LOGIC")
   19.74 +  }
   19.75 +
   19.76 +
   19.77 +  /* plugin instance */
   19.78 +
   19.79 +  var plugin: Plugin = null
   19.80 +
   19.81 +
   19.82 +  /* running provers */
   19.83 +
   19.84 +  def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
   19.85 +}
   19.86 +
   19.87 +
   19.88 +class Plugin extends EBPlugin
   19.89 +{
   19.90 +  /* event buses */
   19.91 +
   19.92 +  val state_update = new Event_Bus[Command]
   19.93 +
   19.94 +
   19.95 +  /* selected state */
   19.96 +
   19.97 +  private var _selected_state: Command = null
   19.98 +  def selected_state = _selected_state
   19.99 +  def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
  19.100 +
  19.101 +
  19.102 +  /* mapping buffer <-> prover */
  19.103 +
  19.104 +  private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
  19.105 +
  19.106 +  private def install(view: View)
  19.107 +  {
  19.108 +    val buffer = view.getBuffer
  19.109 +    val prover_setup = new ProverSetup(buffer)
  19.110 +    mapping.update(buffer, prover_setup)
  19.111 +    prover_setup.activate(view)
  19.112 +  }
  19.113 +
  19.114 +  private def uninstall(view: View) =
  19.115 +    mapping.removeKey(view.getBuffer).get.deactivate
  19.116 +
  19.117 +  def switch_active (view: View) =
  19.118 +    if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
  19.119 +    else install(view)
  19.120 +
  19.121 +  def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
  19.122 +  def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
  19.123 +
  19.124 +
  19.125 +  /* main plugin plumbing */
  19.126 +
  19.127 +  override def handleMessage(msg: EBMessage)
  19.128 +  {
  19.129 +    msg match {
  19.130 +      case epu: EditPaneUpdate =>
  19.131 +        val buffer = epu.getEditPane.getBuffer
  19.132 +        epu.getWhat match {
  19.133 +          case EditPaneUpdate.BUFFER_CHANGED =>
  19.134 +            (mapping get buffer) map (_.theory_view.activate)
  19.135 +          case EditPaneUpdate.BUFFER_CHANGING =>
  19.136 +            if (buffer != null)
  19.137 +              (mapping get buffer) map (_.theory_view.deactivate)
  19.138 +          case _ =>
  19.139 +        }
  19.140 +      case _ =>
  19.141 +    }
  19.142 +  }
  19.143 +
  19.144 +  override def start()
  19.145 +  {
  19.146 +    Isabelle.plugin = this
  19.147 +    Isabelle.system = new Isabelle_System
  19.148 +    if (!Isabelle.system.register_fonts())
  19.149 +      System.err.println("Failed to register Isabelle fonts")
  19.150 +  }
  19.151 +
  19.152 +  override def stop()
  19.153 +  {
  19.154 +    // TODO: proper cleanup
  19.155 +    Isabelle.system = null
  19.156 +    Isabelle.plugin = null
  19.157 +  }
  19.158 +}
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/Tools/jEdit/src/jedit/prover_setup.scala	Tue Dec 08 14:49:01 2009 +0100
    20.3 @@ -0,0 +1,35 @@
    20.4 +/*
    20.5 + * Independent prover sessions for each buffer
    20.6 + *
    20.7 + * @author Fabian Immler, TU Munich
    20.8 + */
    20.9 +
   20.10 +package isabelle.jedit
   20.11 +
   20.12 +
   20.13 +import org.gjt.sp.jedit.{Buffer, View}
   20.14 +
   20.15 +import isabelle.prover.Prover
   20.16 +
   20.17 +
   20.18 +class ProverSetup(buffer: Buffer)
   20.19 +{
   20.20 +  var prover: Prover = null
   20.21 +  var theory_view: TheoryView = null
   20.22 +
   20.23 +  def activate(view: View)
   20.24 +  {
   20.25 +    // TheoryView starts prover
   20.26 +    theory_view = new TheoryView(view.getTextArea)
   20.27 +    prover = theory_view.prover
   20.28 +
   20.29 +    theory_view.activate()
   20.30 +    prover.begin_document(buffer.getName)
   20.31 +  }
   20.32 +
   20.33 +  def deactivate()
   20.34 +  {
   20.35 +    theory_view.deactivate
   20.36 +    prover.stop
   20.37 +  }
   20.38 +}
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Tue Dec 08 14:49:01 2009 +0100
    21.3 @@ -0,0 +1,31 @@
    21.4 +/*
    21.5 + * Dockable window for raw process output
    21.6 + *
    21.7 + * @author Fabian Immler, TU Munich
    21.8 + * @author Johannes Hölzl, TU Munich
    21.9 + */
   21.10 +
   21.11 +package isabelle.jedit
   21.12 +
   21.13 +
   21.14 +import java.awt.{Dimension, Graphics, GridLayout}
   21.15 +import javax.swing.{JPanel, JTextArea, JScrollPane}
   21.16 +
   21.17 +import org.gjt.sp.jedit.View
   21.18 +import org.gjt.sp.jedit.gui.DockableWindowManager
   21.19 +
   21.20 +
   21.21 +class OutputDockable(view : View, position : String) extends JPanel {
   21.22 +
   21.23 +  if (position == DockableWindowManager.FLOATING)
   21.24 +    setPreferredSize(new Dimension(500, 250))
   21.25 +
   21.26 +  setLayout(new GridLayout(1, 1))
   21.27 +  add(new JScrollPane(new JTextArea))
   21.28 +
   21.29 +  def set_text(output_text_view: JTextArea) {
   21.30 +    removeAll()
   21.31 +    add(new JScrollPane(output_text_view))
   21.32 +    revalidate()
   21.33 +  }
   21.34 +}
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 14:49:01 2009 +0100
    22.3 @@ -0,0 +1,111 @@
    22.4 +/*
    22.5 + * Dockable window with rendered state output
    22.6 + *
    22.7 + * @author Fabian Immler, TU Munich
    22.8 + * @author Johannes Hölzl, TU Munich
    22.9 + */
   22.10 +
   22.11 +package isabelle.jedit
   22.12 +
   22.13 +import isabelle.XML
   22.14 +
   22.15 +import java.io.StringReader
   22.16 +import java.awt.{BorderLayout, Dimension}
   22.17 +
   22.18 +import javax.swing.{JButton, JPanel, JScrollPane}
   22.19 +
   22.20 +import java.util.logging.{Logger, Level}
   22.21 +
   22.22 +import org.lobobrowser.html.parser._
   22.23 +import org.lobobrowser.html.test._
   22.24 +import org.lobobrowser.html.gui._
   22.25 +import org.lobobrowser.html._
   22.26 +import org.lobobrowser.html.style.CSSUtilities
   22.27 +import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
   22.28 +
   22.29 +import org.gjt.sp.jedit.jEdit
   22.30 +import org.gjt.sp.jedit.View
   22.31 +import org.gjt.sp.jedit.gui.DockableWindowManager
   22.32 +import org.gjt.sp.jedit.textarea.AntiAlias
   22.33 +
   22.34 +import scala.io.Source
   22.35 +
   22.36 +
   22.37 +class StateViewDockable(view : View, position : String) extends JPanel {
   22.38 +
   22.39 +  // outer panel
   22.40 +  if (position == DockableWindowManager.FLOATING)
   22.41 +    setPreferredSize(new Dimension(500, 250))
   22.42 +  setLayout(new BorderLayout)
   22.43 +
   22.44 +
   22.45 +  // global logging
   22.46 +  
   22.47 +  Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
   22.48 +
   22.49 +
   22.50 +  // document template with styles
   22.51 +
   22.52 +  private def try_file(name: String): String =
   22.53 +  {
   22.54 +    val file = Isabelle.system.platform_file(name)
   22.55 +    if (file.exists) Source.fromFile(file).mkString else ""
   22.56 +  }
   22.57 +
   22.58 +
   22.59 +  // HTML panel
   22.60 +
   22.61 +  val panel = new HtmlPanel
   22.62 +  val ucontext = new SimpleUserAgentContext
   22.63 +  val rcontext = new SimpleHtmlRendererContext(panel, ucontext)
   22.64 +  val doc = {
   22.65 +    val builder = new DocumentBuilderImpl(ucontext, rcontext)
   22.66 +    builder.parse(new InputSourceImpl(new StringReader(
   22.67 +      """<?xml version="1.0" encoding="utf-8"?>
   22.68 +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
   22.69 +  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
   22.70 +<html xmlns="http://www.w3.org/1999/xhtml">
   22.71 +<head>
   22.72 +<style media="all" type="text/css">
   22.73 +""" +
   22.74 +  try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
   22.75 +"""
   22.76 +body {
   22.77 +  font-family: IsabelleText;
   22.78 +  font-size: 14pt;
   22.79 +}
   22.80 +""" +
   22.81 +  try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
   22.82 +"""
   22.83 +</style>
   22.84 +</head>
   22.85 +</html>
   22.86 +""")))
   22.87 +  }
   22.88 +
   22.89 +  val empty_body = XML.document_node(doc, XML.elem(HTML.BODY))
   22.90 +  doc.appendChild(empty_body)
   22.91 +
   22.92 +  panel.setDocument(doc, rcontext)
   22.93 +  add(panel, BorderLayout.CENTER)
   22.94 +
   22.95 +  
   22.96 +  // register for state-view
   22.97 +  Isabelle.plugin.state_update += (cmd => {
   22.98 +    val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
   22.99 +
  22.100 +    Swing_Thread.later {
  22.101 +      val node =
  22.102 +        if (cmd == null) empty_body
  22.103 +        else {
  22.104 +          val xml = XML.elem(HTML.BODY,
  22.105 +            cmd.results(theory_view.current_document).
  22.106 +              map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t))))
  22.107 +          XML.document_node(doc, xml)
  22.108 +        }
  22.109 +      doc.removeChild(doc.getLastChild())
  22.110 +      doc.appendChild(node)
  22.111 +      panel.delayedRelayout(node.asInstanceOf[NodeImpl])
  22.112 +    }
  22.113 +  })
  22.114 +}
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/Tools/jEdit/src/jedit/token_marker.scala	Tue Dec 08 14:49:01 2009 +0100
    23.3 @@ -0,0 +1,154 @@
    23.4 +/*
    23.5 + * include isabelle's command- and keyword-declarations
    23.6 + * live in jEdits syntax-highlighting
    23.7 + *
    23.8 + * @author Fabian Immler, TU Munich
    23.9 + */
   23.10 +
   23.11 +package isabelle.jedit
   23.12 +
   23.13 +
   23.14 +import isabelle.prover.Prover
   23.15 +import isabelle.Markup
   23.16 +
   23.17 +import org.gjt.sp.jedit.buffer.JEditBuffer
   23.18 +import org.gjt.sp.jedit.syntax.{Token => JToken,
   23.19 +  TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
   23.20 +
   23.21 +import java.awt.Color
   23.22 +import java.awt.Font
   23.23 +import javax.swing.text.Segment;
   23.24 +
   23.25 +
   23.26 +object DynamicTokenMarker
   23.27 +{
   23.28 +  /* line context */
   23.29 +
   23.30 +  private val rule_set = new ParserRuleSet("isabelle", "MAIN")
   23.31 +  private class LineContext(val line: Int, prev: LineContext)
   23.32 +    extends TokenMarker.LineContext(rule_set, prev)
   23.33 +
   23.34 +
   23.35 +  /* mapping to jEdit token types */
   23.36 +  // TODO: as properties or CSS style sheet
   23.37 +
   23.38 +  private val choose_byte: Map[String, Byte] =
   23.39 +  {
   23.40 +    import JToken._
   23.41 +    Map[String, Byte](
   23.42 +      // logical entities
   23.43 +      Markup.TCLASS -> LABEL,
   23.44 +      Markup.TYCON -> LABEL,
   23.45 +      Markup.FIXED_DECL -> LABEL,
   23.46 +      Markup.FIXED -> LABEL,
   23.47 +      Markup.CONST_DECL -> LABEL,
   23.48 +      Markup.CONST -> LABEL,
   23.49 +      Markup.FACT_DECL -> LABEL,
   23.50 +      Markup.FACT -> LABEL,
   23.51 +      Markup.DYNAMIC_FACT -> LABEL,
   23.52 +      Markup.LOCAL_FACT_DECL -> LABEL,
   23.53 +      Markup.LOCAL_FACT -> LABEL,
   23.54 +      // inner syntax
   23.55 +      Markup.TFREE -> LITERAL2,
   23.56 +      Markup.FREE -> LITERAL2,
   23.57 +      Markup.TVAR -> LITERAL3,
   23.58 +      Markup.SKOLEM -> LITERAL3,
   23.59 +      Markup.BOUND -> LITERAL3,
   23.60 +      Markup.VAR -> LITERAL3,
   23.61 +      Markup.NUM -> DIGIT,
   23.62 +      Markup.FLOAT -> DIGIT,
   23.63 +      Markup.XNUM -> DIGIT,
   23.64 +      Markup.XSTR -> LITERAL4,
   23.65 +      Markup.LITERAL -> LITERAL4,
   23.66 +      Markup.INNER_COMMENT -> COMMENT1,
   23.67 +      Markup.SORT -> FUNCTION,
   23.68 +      Markup.TYP -> FUNCTION,
   23.69 +      Markup.TERM -> FUNCTION,
   23.70 +      Markup.PROP -> FUNCTION,
   23.71 +      Markup.ATTRIBUTE -> FUNCTION,
   23.72 +      Markup.METHOD -> FUNCTION,
   23.73 +      // ML syntax
   23.74 +      Markup.ML_KEYWORD -> KEYWORD2,
   23.75 +      Markup.ML_IDENT -> NULL,
   23.76 +      Markup.ML_TVAR -> LITERAL3,
   23.77 +      Markup.ML_NUMERAL -> DIGIT,
   23.78 +      Markup.ML_CHAR -> LITERAL1,
   23.79 +      Markup.ML_STRING -> LITERAL1,
   23.80 +      Markup.ML_COMMENT -> COMMENT1,
   23.81 +      Markup.ML_MALFORMED -> INVALID,
   23.82 +      // embedded source text
   23.83 +      Markup.ML_SOURCE -> COMMENT4,
   23.84 +      Markup.DOC_SOURCE -> COMMENT4,
   23.85 +      Markup.ANTIQ -> COMMENT4,
   23.86 +      Markup.ML_ANTIQ -> COMMENT4,
   23.87 +      Markup.DOC_ANTIQ -> COMMENT4,
   23.88 +      // outer syntax
   23.89 +      Markup.IDENT -> NULL,
   23.90 +      Markup.COMMAND -> OPERATOR,
   23.91 +      Markup.KEYWORD -> KEYWORD4,
   23.92 +      Markup.VERBATIM -> COMMENT3,
   23.93 +      Markup.COMMENT -> COMMENT1,
   23.94 +      Markup.CONTROL -> COMMENT3,
   23.95 +      Markup.MALFORMED -> INVALID,
   23.96 +      Markup.STRING -> LITERAL3,
   23.97 +      Markup.ALTSTRING -> LITERAL1
   23.98 +    ).withDefaultValue(NULL)
   23.99 +  }
  23.100 +
  23.101 +  def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
  23.102 +    styles(choose_byte(kind)).getForegroundColor
  23.103 +}
  23.104 +
  23.105 +
  23.106 +class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover)
  23.107 +  extends TokenMarker
  23.108 +{
  23.109 +  override def markTokens(prev: TokenMarker.LineContext,
  23.110 +      handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
  23.111 +  {
  23.112 +    val previous = prev.asInstanceOf[DynamicTokenMarker.LineContext]
  23.113 +    val line = if (prev == null) 0 else previous.line + 1
  23.114 +    val context = new DynamicTokenMarker.LineContext(line, previous)
  23.115 +    val start = buffer.getLineStartOffset(line)
  23.116 +    val stop = start + line_segment.count
  23.117 +
  23.118 +    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
  23.119 +    val document = theory_view.current_document()
  23.120 +    def to: Int => Int = theory_view.to_current(document, _)
  23.121 +    def from: Int => Int = theory_view.from_current(document, _)
  23.122 +
  23.123 +    var next_x = start
  23.124 +    var cmd = document.command_at(from(start))
  23.125 +    while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
  23.126 +      val command = cmd.get
  23.127 +      for {
  23.128 +        markup <- command.highlight(document).flatten
  23.129 +        command_start = command.start(document)
  23.130 +        abs_start = to(command_start + markup.start)
  23.131 +        abs_stop = to(command_start + markup.stop)
  23.132 +        if (abs_stop > start)
  23.133 +        if (abs_start < stop)
  23.134 +        byte = DynamicTokenMarker.choose_byte(markup.info.toString)
  23.135 +        token_start = (abs_start - start) max 0
  23.136 +        token_length =
  23.137 +          (abs_stop - abs_start) -
  23.138 +          ((start - abs_start) max 0) -
  23.139 +          ((abs_stop - stop) max 0)
  23.140 +      } {
  23.141 +        if (start + token_start > next_x)
  23.142 +          handler.handleToken(line_segment, 1,
  23.143 +            next_x - start, start + token_start - next_x, context)
  23.144 +        handler.handleToken(line_segment, byte,
  23.145 +          token_start, token_length, context)
  23.146 +        next_x = start + token_start + token_length
  23.147 +      }
  23.148 +      cmd = document.commands.next(command)
  23.149 +    }
  23.150 +    if (next_x < stop)
  23.151 +      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
  23.152 +
  23.153 +    handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
  23.154 +    handler.setLineContext(context)
  23.155 +    return context
  23.156 +  }
  23.157 +}
    24.1 --- a/src/Tools/jEdit/src/proofdocument/Change.scala	Tue Dec 08 14:29:29 2009 +0100
    24.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.3 @@ -1,54 +0,0 @@
    24.4 -/*
    24.5 - * Changes of plain text
    24.6 - *
    24.7 - * @author Johannes Hölzl, TU Munich
    24.8 - * @author Fabian Immler, TU Munich
    24.9 - */
   24.10 -
   24.11 -package isabelle.proofdocument
   24.12 -
   24.13 -
   24.14 -sealed abstract class Edit
   24.15 -{
   24.16 -  val start: Int
   24.17 -  def before(offset: Int): Int
   24.18 -  def after(offset: Int): Int
   24.19 -}
   24.20 -
   24.21 -
   24.22 -case class Insert(start: Int, text: String) extends Edit
   24.23 -{
   24.24 -  def before(offset: Int): Int =
   24.25 -    if (start > offset) offset
   24.26 -    else (offset - text.length) max start
   24.27 -
   24.28 -  def after(offset: Int): Int =
   24.29 -    if (start <= offset) offset + text.length else offset
   24.30 -}
   24.31 -
   24.32 -
   24.33 -case class Remove(start: Int, text: String) extends Edit
   24.34 -{
   24.35 -  def before(offset: Int): Int =
   24.36 -    if (start <= offset) offset + text.length else offset
   24.37 -
   24.38 -  def after(offset: Int): Int =
   24.39 -    if (start > offset) offset
   24.40 -    else (offset - text.length) max start
   24.41 -}
   24.42 -// TODO: merge multiple inserts?
   24.43 -
   24.44 -
   24.45 -class Change(
   24.46 -  val id: String,
   24.47 -  val parent: Option[Change],
   24.48 -  val edits: List[Edit])
   24.49 -{
   24.50 -  def ancestors(done: Change => Boolean): List[Change] =
   24.51 -    if (done(this)) Nil
   24.52 -    else this :: parent.map(_.ancestors(done)).getOrElse(Nil)
   24.53 -  def ancestors: List[Change] = ancestors(_ => false)
   24.54 -
   24.55 -  override def toString =
   24.56 -    "Change(" + id + " <- " + parent.map(_.id) + ", " + edits + ")"
   24.57 -}
   24.58 \ No newline at end of file
    25.1 --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Dec 08 14:29:29 2009 +0100
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,277 +0,0 @@
    25.4 -/*
    25.5 - * Document as list of commands, consisting of lists of tokens
    25.6 - *
    25.7 - * @author Johannes Hölzl, TU Munich
    25.8 - * @author Fabian Immler, TU Munich
    25.9 - * @author Makarius
   25.10 - */
   25.11 -
   25.12 -package isabelle.proofdocument
   25.13 -
   25.14 -import scala.actors.Actor, Actor._
   25.15 -
   25.16 -import java.util.regex.Pattern
   25.17 -
   25.18 -import isabelle.prover.{Prover, Command, Command_State}
   25.19 -
   25.20 -
   25.21 -object ProofDocument
   25.22 -{
   25.23 -  // Be careful when changing this regex. Not only must it handle the
   25.24 -  // spurious end of a token but also:  
   25.25 -  // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
   25.26 -  // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
   25.27 -  
   25.28 -  val token_pattern = 
   25.29 -    Pattern.compile(
   25.30 -      "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
   25.31 -      "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
   25.32 -      "(\\?'?|')[A-Za-z_0-9.]*|" + 
   25.33 -      "[A-Za-z_0-9.]+|" + 
   25.34 -      "[!#$%&*+-/<=>?@^_|~]+|" +
   25.35 -      "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
   25.36 -      "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
   25.37 -      "[()\\[\\]{}:;]", Pattern.MULTILINE)
   25.38 -
   25.39 -  val empty =
   25.40 -    new ProofDocument(isabelle.jedit.Isabelle.system.id(),
   25.41 -      Linear_Set(), Map(), Linear_Set(), Map(), _ => false)
   25.42 -
   25.43 -  type StructureChange = List[(Option[Command], Option[Command])]
   25.44 -
   25.45 -}
   25.46 -
   25.47 -class ProofDocument(
   25.48 -  val id: String,
   25.49 -  val tokens: Linear_Set[Token],
   25.50 -  val token_start: Map[Token, Int],
   25.51 -  val commands: Linear_Set[Command],
   25.52 -  var states: Map[Command, Command_State],   // FIXME immutable
   25.53 -  is_command_keyword: String => Boolean)
   25.54 -{
   25.55 -  import ProofDocument.StructureChange
   25.56 -
   25.57 -  def set_command_keyword(f: String => Boolean): ProofDocument =
   25.58 -    new ProofDocument(id, tokens, token_start, commands, states, f)
   25.59 -
   25.60 -  def content = Token.string_from_tokens(Nil ++ tokens, token_start)
   25.61 -
   25.62 -
   25.63 -  
   25.64 -  /** token view **/
   25.65 -
   25.66 -  def text_changed(change: Change): (ProofDocument, StructureChange) =
   25.67 -  {
   25.68 -    def edit_doc(doc_chgs: (ProofDocument, StructureChange), edit: Edit) = {
   25.69 -      val (doc, chgs) = doc_chgs
   25.70 -      val (new_doc, chg) = doc.text_edit(edit, change.id)
   25.71 -      (new_doc, chgs ++ chg)
   25.72 -    }
   25.73 -    ((this, Nil: StructureChange) /: change.edits)(edit_doc)
   25.74 -  }
   25.75 -
   25.76 -  def text_edit(e: Edit, id: String): (ProofDocument, StructureChange) =
   25.77 -  {
   25.78 -    case class TextChange(start: Int, added: String, removed: String)
   25.79 -    val change = e match {
   25.80 -      case Insert(s, a) => TextChange(s, a, "")
   25.81 -      case Remove(s, r) => TextChange(s, "", r)
   25.82 -    }
   25.83 -    //indices of tokens
   25.84 -    var start: Map[Token, Int] = token_start
   25.85 -    def stop(t: Token) = start(t) + t.length
   25.86 -    // split old token lists
   25.87 -    val tokens = Nil ++ this.tokens
   25.88 -    val (begin, remaining) = tokens.span(stop(_) < change.start)
   25.89 -    val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed.length)
   25.90 -    // update indices
   25.91 -    start = end.foldLeft(start)((s, t) =>
   25.92 -      s + (t -> (s(t) + change.added.length - change.removed.length)))
   25.93 -
   25.94 -    val split_begin = removed.takeWhile(start(_) < change.start).
   25.95 -      map (t => {
   25.96 -          val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind)
   25.97 -          start += (split_tok -> start(t))
   25.98 -          split_tok
   25.99 -        })
  25.100 -
  25.101 -    val split_end = removed.dropWhile(stop(_) < change.start + change.removed.length).
  25.102 -      map (t => {
  25.103 -          val split_tok =
  25.104 -            new Token(t.content.substring(change.start + change.removed.length - start(t)), t.kind)
  25.105 -          start += (split_tok -> start(t))
  25.106 -          split_tok
  25.107 -        })
  25.108 -    // update indices
  25.109 -    start = removed.foldLeft (start) ((s, t) => s - t)
  25.110 -    start = split_end.foldLeft (start) ((s, t) =>
  25.111 -    s + (t -> (change.start + change.added.length)))
  25.112 -
  25.113 -    val ins = new Token(change.added, Token.Kind.OTHER)
  25.114 -    start += (ins -> change.start)
  25.115 -    
  25.116 -    var invalid_tokens = split_begin ::: ins :: split_end ::: end
  25.117 -    var new_tokens: List[Token] = Nil
  25.118 -    var old_suffix: List[Token] = Nil
  25.119 -
  25.120 -    val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
  25.121 -    val matcher =
  25.122 -      ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
  25.123 -
  25.124 -    while (matcher.find() && invalid_tokens != Nil) {
  25.125 -			val kind =
  25.126 -        if (is_command_keyword(matcher.group))
  25.127 -          Token.Kind.COMMAND_START
  25.128 -        else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
  25.129 -          Token.Kind.COMMENT
  25.130 -        else
  25.131 -          Token.Kind.OTHER
  25.132 -      val new_token = new Token(matcher.group, kind)
  25.133 -      start += (new_token -> (match_start + matcher.start))
  25.134 -      new_tokens ::= new_token
  25.135 -
  25.136 -      invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token))
  25.137 -      invalid_tokens match {
  25.138 -        case t :: ts =>
  25.139 -          if (start(t) == start(new_token) &&
  25.140 -              start(t) > change.start + change.added.length) {
  25.141 -          old_suffix = t :: ts
  25.142 -          new_tokens = new_tokens.tail
  25.143 -          invalid_tokens = Nil
  25.144 -        }
  25.145 -        case _ =>
  25.146 -      }
  25.147 -    }
  25.148 -    val insert = new_tokens.reverse
  25.149 -    val new_token_list = begin ::: insert ::: old_suffix
  25.150 -    token_changed(id, begin.lastOption, insert,
  25.151 -      old_suffix.firstOption, new_token_list, start)
  25.152 -  }
  25.153 -
  25.154 -  
  25.155 -  /** command view **/
  25.156 -
  25.157 -  private def token_changed(
  25.158 -    new_id: String,
  25.159 -    before_change: Option[Token],
  25.160 -    inserted_tokens: List[Token],
  25.161 -    after_change: Option[Token],
  25.162 -    new_tokens: List[Token],
  25.163 -    new_token_start: Map[Token, Int]):
  25.164 -  (ProofDocument, StructureChange) =
  25.165 -  {
  25.166 -    val new_tokenset = Linear_Set[Token]() ++ new_tokens
  25.167 -    val cmd_before_change = before_change match {
  25.168 -      case None => None
  25.169 -      case Some(bc) =>
  25.170 -        val cmd_with_bc = commands.find(_.contains(bc)).get
  25.171 -        if (cmd_with_bc.tokens.last == bc) {
  25.172 -          if (new_tokenset.next(bc).map(_.is_start).getOrElse(true))
  25.173 -            Some(cmd_with_bc)
  25.174 -          else commands.prev(cmd_with_bc)
  25.175 -        }
  25.176 -        else commands.prev(cmd_with_bc)
  25.177 -    }
  25.178 -
  25.179 -    val cmd_after_change = after_change match {
  25.180 -      case None => None
  25.181 -      case Some(ac) =>
  25.182 -        val cmd_with_ac = commands.find(_.contains(ac)).get
  25.183 -        if (ac.is_start)
  25.184 -          Some(cmd_with_ac)
  25.185 -        else
  25.186 -          commands.next(cmd_with_ac)
  25.187 -    }
  25.188 -
  25.189 -    val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1).
  25.190 -      takeWhile(Some(_) != cmd_after_change)
  25.191 -
  25.192 -    // calculate inserted commands
  25.193 -    def tokens_to_commands(tokens: List[Token]): List[Command]= {
  25.194 -      tokens match {
  25.195 -        case Nil => Nil
  25.196 -        case t :: ts =>
  25.197 -          val (cmd, rest) =
  25.198 -            ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
  25.199 -          new Command(t :: cmd, new_token_start) :: tokens_to_commands(rest)
  25.200 -      }
  25.201 -    }
  25.202 -
  25.203 -    val split_begin =
  25.204 -      if (before_change.isDefined) {
  25.205 -        val changed =
  25.206 -          if (cmd_before_change.isDefined)
  25.207 -            new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1)
  25.208 -          else new_tokenset
  25.209 -        if (changed.exists(_ == before_change.get))
  25.210 -          changed.takeWhile(_ != before_change.get).toList :::
  25.211 -            List(before_change.get)
  25.212 -        else Nil
  25.213 -      } else Nil
  25.214 -
  25.215 -    val split_end =
  25.216 -      if (after_change.isDefined) {
  25.217 -        val unchanged = new_tokens.dropWhile(_ != after_change.get)
  25.218 -        if(cmd_after_change.isDefined) {
  25.219 -          if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
  25.220 -            unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
  25.221 -          else Nil
  25.222 -        } else {
  25.223 -          unchanged
  25.224 -        }
  25.225 -      } else Nil
  25.226 -
  25.227 -    val rescan_begin =
  25.228 -      split_begin :::
  25.229 -        before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens)
  25.230 -    val rescanning_tokens =
  25.231 -      after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) :::
  25.232 -        split_end
  25.233 -    val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
  25.234 -
  25.235 -    // build new document
  25.236 -    val new_commandset = commands.
  25.237 -      delete_between(cmd_before_change, cmd_after_change).
  25.238 -      append_after(cmd_before_change, inserted_commands)
  25.239 -
  25.240 -
  25.241 -    val doc =
  25.242 -      new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
  25.243 -        states -- removed_commands, is_command_keyword)
  25.244 -
  25.245 -    val removes =
  25.246 -      for (cmd <- removed_commands) yield (cmd_before_change -> None)
  25.247 -    val inserts =
  25.248 -      for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd))
  25.249 -
  25.250 -    return (doc, removes.toList ++ inserts)
  25.251 -  }
  25.252 -
  25.253 -  val commands_offsets = {
  25.254 -    var last_stop = 0
  25.255 -    (for (c <- commands) yield {
  25.256 -      val r = c -> (last_stop,c.stop(this))
  25.257 -      last_stop = c.stop(this)
  25.258 -      r
  25.259 -    }).toArray
  25.260 -  }
  25.261 -
  25.262 -  def command_at(pos: Int): Option[Command] =
  25.263 -    find_command(pos, 0, commands_offsets.length)
  25.264 -
  25.265 -  // use a binary search to find commands for a given offset
  25.266 -  private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] =
  25.267 -  {
  25.268 -    val middle_index = (array_start + array_stop) / 2
  25.269 -    if (middle_index >= commands_offsets.length) return None
  25.270 -    val (middle, (start, stop)) = commands_offsets(middle_index)
  25.271 -    // does middle contain pos?
  25.272 -    if (start <= pos && pos < stop)
  25.273 -      Some(middle)
  25.274 -    else if (start > pos)
  25.275 -      find_command(pos, array_start, middle_index)
  25.276 -    else if (stop <= pos)
  25.277 -      find_command(pos, middle_index + 1, array_stop)
  25.278 -    else error("impossible")
  25.279 -  }
  25.280 -}
    26.1 --- a/src/Tools/jEdit/src/proofdocument/Token.scala	Tue Dec 08 14:29:29 2009 +0100
    26.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.3 @@ -1,42 +0,0 @@
    26.4 -/*
    26.5 - * Document tokens as text ranges
    26.6 - *
    26.7 - * @author Johannes Hölzl, TU Munich
    26.8 - * @author Fabian Immler, TU Munich
    26.9 - */
   26.10 -
   26.11 -package isabelle.proofdocument
   26.12 -
   26.13 -
   26.14 -import isabelle.prover.Command
   26.15 -
   26.16 -
   26.17 -object Token {
   26.18 -  object Kind extends Enumeration
   26.19 -  {
   26.20 -    val COMMAND_START = Value("COMMAND_START")
   26.21 -    val COMMENT = Value("COMMENT")
   26.22 -    val OTHER = Value("OTHER")
   26.23 -  }
   26.24 -
   26.25 -  def string_from_tokens(tokens: List[Token], starts: Token => Int): String = {
   26.26 -    def stop(t: Token) = starts(t) + t.length
   26.27 -    tokens match {
   26.28 -      case Nil => ""
   26.29 -      case tok :: toks =>
   26.30 -        val (res, _) = toks.foldLeft(tok.content, stop(tok))((a, token) =>
   26.31 -          (a._1 + " " * (starts(token) - a._2) + token.content, stop(token)))
   26.32 -        res
   26.33 -    }
   26.34 -  }
   26.35 -
   26.36 -}
   26.37 -
   26.38 -class Token(
   26.39 -  val content: String,
   26.40 -  val kind: Token.Kind.Value)
   26.41 -{
   26.42 -  override def toString = content
   26.43 -  val length = content.length
   26.44 -  val is_start = kind == Token.Kind.COMMAND_START || kind == Token.Kind.COMMENT
   26.45 -}
    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/src/Tools/jEdit/src/proofdocument/change.scala	Tue Dec 08 14:49:01 2009 +0100
    27.3 @@ -0,0 +1,54 @@
    27.4 +/*
    27.5 + * Changes of plain text
    27.6 + *
    27.7 + * @author Johannes Hölzl, TU Munich
    27.8 + * @author Fabian Immler, TU Munich
    27.9 + */
   27.10 +
   27.11 +package isabelle.proofdocument
   27.12 +
   27.13 +
   27.14 +sealed abstract class Edit
   27.15 +{
   27.16 +  val start: Int
   27.17 +  def before(offset: Int): Int
   27.18 +  def after(offset: Int): Int
   27.19 +}
   27.20 +
   27.21 +
   27.22 +case class Insert(start: Int, text: String) extends Edit
   27.23 +{
   27.24 +  def before(offset: Int): Int =
   27.25 +    if (start > offset) offset
   27.26 +    else (offset - text.length) max start
   27.27 +
   27.28 +  def after(offset: Int): Int =
   27.29 +    if (start <= offset) offset + text.length else offset
   27.30 +}
   27.31 +
   27.32 +
   27.33 +case class Remove(start: Int, text: String) extends Edit
   27.34 +{
   27.35 +  def before(offset: Int): Int =
   27.36 +    if (start <= offset) offset + text.length else offset
   27.37 +
   27.38 +  def after(offset: Int): Int =
   27.39 +    if (start > offset) offset
   27.40 +    else (offset - text.length) max start
   27.41 +}
   27.42 +// TODO: merge multiple inserts?
   27.43 +
   27.44 +
   27.45 +class Change(
   27.46 +  val id: String,
   27.47 +  val parent: Option[Change],
   27.48 +  val edits: List[Edit])
   27.49 +{
   27.50 +  def ancestors(done: Change => Boolean): List[Change] =
   27.51 +    if (done(this)) Nil
   27.52 +    else this :: parent.map(_.ancestors(done)).getOrElse(Nil)
   27.53 +  def ancestors: List[Change] = ancestors(_ => false)
   27.54 +
   27.55 +  override def toString =
   27.56 +    "Change(" + id + " <- " + parent.map(_.id) + ", " + edits + ")"
   27.57 +}
   27.58 \ No newline at end of file
    28.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.2 +++ b/src/Tools/jEdit/src/proofdocument/command.scala	Tue Dec 08 14:49:01 2009 +0100
    28.3 @@ -0,0 +1,124 @@
    28.4 +/*
    28.5 + * Prover commands with semantic state
    28.6 + *
    28.7 + * @author Johannes Hölzl, TU Munich
    28.8 + * @author Fabian Immler, TU Munich
    28.9 + */
   28.10 +
   28.11 +package isabelle.prover
   28.12 +
   28.13 +
   28.14 +import scala.actors.Actor, Actor._
   28.15 +
   28.16 +import scala.collection.mutable
   28.17 +
   28.18 +import isabelle.proofdocument.{Token, ProofDocument}
   28.19 +import isabelle.jedit.{Isabelle, Plugin}
   28.20 +import isabelle.XML
   28.21 +
   28.22 +
   28.23 +trait Accumulator extends Actor
   28.24 +{
   28.25 +  start() // start actor
   28.26 +
   28.27 +  protected var _state: State
   28.28 +  def state = _state
   28.29 +
   28.30 +  override def act() {
   28.31 +    loop {
   28.32 +      react {
   28.33 +        case (prover: Prover, message: XML.Tree) => _state = _state.+(prover, message)
   28.34 +        case bad => System.err.println("prover: ignoring bad message " + bad)
   28.35 +      }
   28.36 +    }
   28.37 +  }
   28.38 +}
   28.39 +
   28.40 +
   28.41 +object Command
   28.42 +{
   28.43 +  object Status extends Enumeration
   28.44 +  {
   28.45 +    val UNPROCESSED = Value("UNPROCESSED")
   28.46 +    val FINISHED = Value("FINISHED")
   28.47 +    val FAILED = Value("FAILED")
   28.48 +  }
   28.49 +
   28.50 +  case class HighlightInfo(highlight: String) { override def toString = highlight }
   28.51 +  case class TypeInfo(ty: String)
   28.52 +  case class RefInfo(file: Option[String], line: Option[Int],
   28.53 +    command_id: Option[String], offset: Option[Int])
   28.54 +}
   28.55 +
   28.56 +
   28.57 +class Command(
   28.58 +    val tokens: List[Token],
   28.59 +    val starts: Map[Token, Int]) extends Accumulator
   28.60 +{
   28.61 +  require(!tokens.isEmpty)
   28.62 +
   28.63 +  val id = Isabelle.system.id()
   28.64 +  override def hashCode = id.hashCode
   28.65 +
   28.66 +
   28.67 +  /* content */
   28.68 +
   28.69 +  override def toString = name
   28.70 +
   28.71 +  val name = tokens.head.content
   28.72 +  val content: String = Token.string_from_tokens(tokens, starts)
   28.73 +  def content(i: Int, j: Int): String = content.substring(i, j)
   28.74 +  val symbol_index = new Symbol.Index(content)
   28.75 +
   28.76 +  def start(doc: ProofDocument) = doc.token_start(tokens.first)
   28.77 +  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
   28.78 +
   28.79 +  def contains(p: Token) = tokens.contains(p)
   28.80 +
   28.81 +  protected override var _state = new State(this)
   28.82 +
   28.83 +
   28.84 +  /* markup */
   28.85 +
   28.86 +  lazy val empty_markup = new Markup_Text(Nil, content)
   28.87 +
   28.88 +  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
   28.89 +  {
   28.90 +    val start = symbol_index.decode(begin)
   28.91 +    val stop = symbol_index.decode(end)
   28.92 +    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
   28.93 +  }
   28.94 +
   28.95 +
   28.96 +  /* results, markup, ... */
   28.97 +
   28.98 +  private val empty_cmd_state = new Command_State(this)
   28.99 +  private def cmd_state(doc: ProofDocument) =
  28.100 +    doc.states.getOrElse(this, empty_cmd_state)
  28.101 +
  28.102 +  def status(doc: ProofDocument) = cmd_state(doc).state.status
  28.103 +  def results(doc: ProofDocument) = cmd_state(doc).results
  28.104 +  def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
  28.105 +  def highlight(doc: ProofDocument) = cmd_state(doc).highlight
  28.106 +  def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
  28.107 +  def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
  28.108 +}
  28.109 +
  28.110 +
  28.111 +class Command_State(val command: Command) extends Accumulator
  28.112 +{
  28.113 +  protected override var _state = new State(command)
  28.114 +
  28.115 +  def results: List[XML.Tree] =
  28.116 +    command.state.results ::: state.results
  28.117 +
  28.118 +  def markup_root: Markup_Text =
  28.119 +    (command.state.markup_root /: state.markup_root.markup)(_ + _)
  28.120 +
  28.121 +  def type_at(pos: Int): Option[String] = state.type_at(pos)
  28.122 +
  28.123 +  def ref_at(pos: Int): Option[Markup_Node] = state.ref_at(pos)
  28.124 +
  28.125 +  def highlight: Markup_Text =
  28.126 +    (command.state.highlight /: state.highlight.markup)(_ + _)
  28.127 +}
  28.128 \ No newline at end of file
    29.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.2 +++ b/src/Tools/jEdit/src/proofdocument/markup_node.scala	Tue Dec 08 14:49:01 2009 +0100
    29.3 @@ -0,0 +1,111 @@
    29.4 +/*
    29.5 + * Document markup nodes, with connection to Swing tree model
    29.6 + *
    29.7 + * @author Fabian Immler, TU Munich
    29.8 + */
    29.9 +
   29.10 +package isabelle.prover
   29.11 +
   29.12 +
   29.13 +import javax.swing.tree.DefaultMutableTreeNode
   29.14 +
   29.15 +import isabelle.proofdocument.ProofDocument
   29.16 +
   29.17 +
   29.18 +class Markup_Node(val start: Int, val stop: Int, val info: Any)
   29.19 +{
   29.20 +  def fits_into(that: Markup_Node): Boolean =
   29.21 +    that.start <= this.start && this.stop <= that.stop
   29.22 +}
   29.23 +
   29.24 +
   29.25 +class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
   29.26 +{
   29.27 +  def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
   29.28 +
   29.29 +  private def add(branch: Markup_Tree) =   // FIXME avoid sort
   29.30 +    set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
   29.31 +
   29.32 +  private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
   29.33 +
   29.34 +  def + (new_tree: Markup_Tree): Markup_Tree =
   29.35 +  {
   29.36 +    val new_node = new_tree.node
   29.37 +    if (new_node fits_into node) {
   29.38 +      var inserted = false
   29.39 +      val new_branches =
   29.40 +        branches.map(branch =>
   29.41 +          if ((new_node fits_into branch.node) && !inserted) {
   29.42 +            inserted = true
   29.43 +            branch + new_tree
   29.44 +          }
   29.45 +          else branch)
   29.46 +      if (!inserted) {
   29.47 +        // new_tree did not fit into children of this
   29.48 +        // -> insert between this and its branches
   29.49 +        val fitting = branches filter(_.node fits_into new_node)
   29.50 +        (this remove fitting) add ((new_tree /: fitting)(_ + _))
   29.51 +      }
   29.52 +      else set_branches(new_branches)
   29.53 +    }
   29.54 +    else {
   29.55 +      System.err.println("ignored nonfitting markup: " + new_node)
   29.56 +      this
   29.57 +    }
   29.58 +  }
   29.59 +
   29.60 +  def flatten: List[Markup_Node] =
   29.61 +  {
   29.62 +    var next_x = node.start
   29.63 +    if (branches.isEmpty) List(this.node)
   29.64 +    else {
   29.65 +      val filled_gaps =
   29.66 +        for {
   29.67 +          child <- branches
   29.68 +          markups =
   29.69 +            if (next_x < child.node.start)
   29.70 +              new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
   29.71 +            else child.flatten
   29.72 +          update = (next_x = child.node.stop)
   29.73 +          markup <- markups
   29.74 +        } yield markup
   29.75 +      if (next_x < node.stop)
   29.76 +        filled_gaps + new Markup_Node(next_x, node.stop, node.info)
   29.77 +      else filled_gaps
   29.78 +    }
   29.79 +  }
   29.80 +}
   29.81 +
   29.82 +
   29.83 +class Markup_Text(val markup: List[Markup_Tree], val content: String)
   29.84 +{
   29.85 +  private lazy val root =
   29.86 +    new Markup_Tree(new Markup_Node(0, content.length, None), markup)
   29.87 +
   29.88 +  def + (new_tree: Markup_Tree): Markup_Text =
   29.89 +    new Markup_Text((root + new_tree).branches, content)
   29.90 +
   29.91 +  def filter(pred: Markup_Node => Boolean): Markup_Text =
   29.92 +  {
   29.93 +    def filt(tree: Markup_Tree): List[Markup_Tree] =
   29.94 +    {
   29.95 +      val branches = tree.branches.flatMap(filt(_))
   29.96 +      if (pred(tree.node)) List(tree.set_branches(branches))
   29.97 +      else branches
   29.98 +    }
   29.99 +    new Markup_Text(markup.flatMap(filt(_)), content)
  29.100 +  }
  29.101 +
  29.102 +  def flatten: List[Markup_Node] = markup.flatten(_.flatten)
  29.103 +
  29.104 +  def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
  29.105 +  {
  29.106 +    def swing(tree: Markup_Tree): DefaultMutableTreeNode =
  29.107 +    {
  29.108 +      val node = swing_node(tree.node)
  29.109 +      tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
  29.110 +      node
  29.111 +    }
  29.112 +    swing(root)
  29.113 +  }
  29.114 +}
    30.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.2 +++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala	Tue Dec 08 14:49:01 2009 +0100
    30.3 @@ -0,0 +1,277 @@
    30.4 +/*
    30.5 + * Document as list of commands, consisting of lists of tokens
    30.6 + *
    30.7 + * @author Johannes Hölzl, TU Munich
    30.8 + * @author Fabian Immler, TU Munich
    30.9 + * @author Makarius
   30.10 + */
   30.11 +
   30.12 +package isabelle.proofdocument
   30.13 +
   30.14 +import scala.actors.Actor, Actor._
   30.15 +
   30.16 +import java.util.regex.Pattern
   30.17 +
   30.18 +import isabelle.prover.{Prover, Command, Command_State}
   30.19 +
   30.20 +
   30.21 +object ProofDocument
   30.22 +{
   30.23 +  // Be careful when changing this regex. Not only must it handle the
   30.24 +  // spurious end of a token but also:  
   30.25 +  // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
   30.26 +  // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
   30.27 +  
   30.28 +  val token_pattern = 
   30.29 +    Pattern.compile(
   30.30 +      "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
   30.31 +      "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
   30.32 +      "(\\?'?|')[A-Za-z_0-9.]*|" + 
   30.33 +      "[A-Za-z_0-9.]+|" + 
   30.34 +      "[!#$%&*+-/<=>?@^_|~]+|" +
   30.35 +      "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
   30.36 +      "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
   30.37 +      "[()\\[\\]{}:;]", Pattern.MULTILINE)
   30.38 +
   30.39 +  val empty =
   30.40 +    new ProofDocument(isabelle.jedit.Isabelle.system.id(),
   30.41 +      Linear_Set(), Map(), Linear_Set(), Map(), _ => false)
   30.42 +
   30.43 +  type StructureChange = List[(Option[Command], Option[Command])]
   30.44 +
   30.45 +}
   30.46 +
   30.47 +class ProofDocument(
   30.48 +  val id: String,
   30.49 +  val tokens: Linear_Set[Token],
   30.50 +  val token_start: Map[Token, Int],
   30.51 +  val commands: Linear_Set[Command],
   30.52 +  var states: Map[Command, Command_State],   // FIXME immutable
   30.53 +  is_command_keyword: String => Boolean)
   30.54 +{
   30.55 +  import ProofDocument.StructureChange
   30.56 +
   30.57 +  def set_command_keyword(f: String => Boolean): ProofDocument =
   30.58 +    new ProofDocument(id, tokens, token_start, commands, states, f)
   30.59 +
   30.60 +  def content = Token.string_from_tokens(Nil ++ tokens, token_start)
   30.61 +
   30.62 +
   30.63 +  
   30.64 +  /** token view **/
   30.65 +
   30.66 +  def text_changed(change: Change): (ProofDocument, StructureChange) =
   30.67 +  {
   30.68 +    def edit_doc(doc_chgs: (ProofDocument, StructureChange), edit: Edit) = {
   30.69 +      val (doc, chgs) = doc_chgs
   30.70 +      val (new_doc, chg) = doc.text_edit(edit, change.id)
   30.71 +      (new_doc, chgs ++ chg)
   30.72 +    }
   30.73 +    ((this, Nil: StructureChange) /: change.edits)(edit_doc)
   30.74 +  }
   30.75 +
   30.76 +  def text_edit(e: Edit, id: String): (ProofDocument, StructureChange) =
   30.77 +  {
   30.78 +    case class TextChange(start: Int, added: String, removed: String)
   30.79 +    val change = e match {
   30.80 +      case Insert(s, a) => TextChange(s, a, "")
   30.81 +      case Remove(s, r) => TextChange(s, "", r)
   30.82 +    }
   30.83 +    //indices of tokens
   30.84 +    var start: Map[Token, Int] = token_start
   30.85 +    def stop(t: Token) = start(t) + t.length
   30.86 +    // split old token lists
   30.87 +    val tokens = Nil ++ this.tokens
   30.88 +    val (begin, remaining) = tokens.span(stop(_) < change.start)
   30.89 +    val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed.length)
   30.90 +    // update indices
   30.91 +    start = end.foldLeft(start)((s, t) =>
   30.92 +      s + (t -> (s(t) + change.added.length - change.removed.length)))
   30.93 +
   30.94 +    val split_begin = removed.takeWhile(start(_) < change.start).
   30.95 +      map (t => {
   30.96 +          val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind)
   30.97 +          start += (split_tok -> start(t))
   30.98 +          split_tok
   30.99 +        })
  30.100 +
  30.101 +    val split_end = removed.dropWhile(stop(_) < change.start + change.removed.length).
  30.102 +      map (t => {
  30.103 +          val split_tok =
  30.104 +            new Token(t.content.substring(change.start + change.removed.length - start(t)), t.kind)
  30.105 +          start += (split_tok -> start(t))
  30.106 +          split_tok
  30.107 +        })
  30.108 +    // update indices
  30.109 +    start = removed.foldLeft (start) ((s, t) => s - t)
  30.110 +    start = split_end.foldLeft (start) ((s, t) =>
  30.111 +    s + (t -> (change.start + change.added.length)))
  30.112 +
  30.113 +    val ins = new Token(change.added, Token.Kind.OTHER)
  30.114 +    start += (ins -> change.start)
  30.115 +    
  30.116 +    var invalid_tokens = split_begin ::: ins :: split_end ::: end
  30.117 +    var new_tokens: List[Token] = Nil
  30.118 +    var old_suffix: List[Token] = Nil
  30.119 +
  30.120 +    val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
  30.121 +    val matcher =
  30.122 +      ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
  30.123 +
  30.124 +    while (matcher.find() && invalid_tokens != Nil) {
  30.125 +			val kind =
  30.126 +        if (is_command_keyword(matcher.group))
  30.127 +          Token.Kind.COMMAND_START
  30.128 +        else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
  30.129 +          Token.Kind.COMMENT
  30.130 +        else
  30.131 +          Token.Kind.OTHER
  30.132 +      val new_token = new Token(matcher.group, kind)
  30.133 +      start += (new_token -> (match_start + matcher.start))
  30.134 +      new_tokens ::= new_token
  30.135 +
  30.136 +      invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token))
  30.137 +      invalid_tokens match {
  30.138 +        case t :: ts =>
  30.139 +          if (start(t) == start(new_token) &&
  30.140 +              start(t) > change.start + change.added.length) {
  30.141 +          old_suffix = t :: ts
  30.142 +          new_tokens = new_tokens.tail
  30.143 +          invalid_tokens = Nil
  30.144 +        }
  30.145 +        case _ =>
  30.146 +      }
  30.147 +    }
  30.148 +    val insert = new_tokens.reverse
  30.149 +    val new_token_list = begin ::: insert ::: old_suffix
  30.150 +    token_changed(id, begin.lastOption, insert,
  30.151 +      old_suffix.firstOption, new_token_list, start)
  30.152 +  }
  30.153 +
  30.154 +  
  30.155 +  /** command view **/
  30.156 +
  30.157 +  private def token_changed(
  30.158 +    new_id: String,
  30.159 +    before_change: Option[Token],
  30.160 +    inserted_tokens: List[Token],
  30.161 +    after_change: Option[Token],
  30.162 +    new_tokens: List[Token],
  30.163 +    new_token_start: Map[Token, Int]):
  30.164 +  (ProofDocument, StructureChange) =
  30.165 +  {
  30.166 +    val new_tokenset = Linear_Set[Token]() ++ new_tokens
  30.167 +    val cmd_before_change = before_change match {
  30.168 +      case None => None
  30.169 +      case Some(bc) =>
  30.170 +        val cmd_with_bc = commands.find(_.contains(bc)).get
  30.171 +        if (cmd_with_bc.tokens.last == bc) {
  30.172 +          if (new_tokenset.next(bc).map(_.is_start).getOrElse(true))
  30.173 +            Some(cmd_with_bc)
  30.174 +          else commands.prev(cmd_with_bc)
  30.175 +        }
  30.176 +        else commands.prev(cmd_with_bc)
  30.177 +    }
  30.178 +
  30.179 +    val cmd_after_change = after_change match {
  30.180 +      case None => None
  30.181 +      case Some(ac) =>
  30.182 +        val cmd_with_ac = commands.find(_.contains(ac)).get
  30.183 +        if (ac.is_start)
  30.184 +          Some(cmd_with_ac)
  30.185 +        else
  30.186 +          commands.next(cmd_with_ac)
  30.187 +    }
  30.188 +
  30.189 +    val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1).
  30.190 +      takeWhile(Some(_) != cmd_after_change)
  30.191 +
  30.192 +    // calculate inserted commands
  30.193 +    def tokens_to_commands(tokens: List[Token]): List[Command]= {
  30.194 +      tokens match {
  30.195 +        case Nil => Nil
  30.196 +        case t :: ts =>
  30.197 +          val (cmd, rest) =
  30.198 +            ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
  30.199 +          new Command(t :: cmd, new_token_start) :: tokens_to_commands(rest)
  30.200 +      }
  30.201 +    }
  30.202 +
  30.203 +    val split_begin =
  30.204 +      if (before_change.isDefined) {
  30.205 +        val changed =
  30.206 +          if (cmd_before_change.isDefined)
  30.207 +            new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1)
  30.208 +          else new_tokenset
  30.209 +        if (changed.exists(_ == before_change.get))
  30.210 +          changed.takeWhile(_ != before_change.get).toList :::
  30.211 +            List(before_change.get)
  30.212 +        else Nil
  30.213 +      } else Nil
  30.214 +
  30.215 +    val split_end =
  30.216 +      if (after_change.isDefined) {
  30.217 +        val unchanged = new_tokens.dropWhile(_ != after_change.get)
  30.218 +        if(cmd_after_change.isDefined) {
  30.219 +          if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
  30.220 +            unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
  30.221 +          else Nil
  30.222 +        } else {
  30.223 +          unchanged
  30.224 +        }
  30.225 +      } else Nil
  30.226 +
  30.227 +    val rescan_begin =
  30.228 +      split_begin :::
  30.229 +        before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens)
  30.230 +    val rescanning_tokens =
  30.231 +      after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) :::
  30.232 +        split_end
  30.233 +    val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
  30.234 +
  30.235 +    // build new document
  30.236 +    val new_commandset = commands.
  30.237 +      delete_between(cmd_before_change, cmd_after_change).
  30.238 +      append_after(cmd_before_change, inserted_commands)
  30.239 +
  30.240 +
  30.241 +    val doc =
  30.242 +      new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
  30.243 +        states -- removed_commands, is_command_keyword)
  30.244 +
  30.245 +    val removes =
  30.246 +      for (cmd <- removed_commands) yield (cmd_before_change -> None)
  30.247 +    val inserts =
  30.248 +      for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd))
  30.249 +
  30.250 +    return (doc, removes.toList ++ inserts)
  30.251 +  }
  30.252 +
  30.253 +  val commands_offsets = {
  30.254 +    var last_stop = 0
  30.255 +    (for (c <- commands) yield {
  30.256 +      val r = c -> (last_stop,c.stop(this))
  30.257 +      last_stop = c.stop(this)
  30.258 +      r
  30.259 +    }).toArray
  30.260 +  }
  30.261 +
  30.262 +  def command_at(pos: Int): Option[Command] =
  30.263 +    find_command(pos, 0, commands_offsets.length)
  30.264 +
  30.265 +  // use a binary search to find commands for a given offset
  30.266 +  private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] =
  30.267 +  {
  30.268 +    val middle_index = (array_start + array_stop) / 2
  30.269 +    if (middle_index >= commands_offsets.length) return None
  30.270 +    val (middle, (start, stop)) = commands_offsets(middle_index)
  30.271 +    // does middle contain pos?
  30.272 +    if (start <= pos && pos < stop)
  30.273 +      Some(middle)
  30.274 +    else if (start > pos)
  30.275 +      find_command(pos, array_start, middle_index)
  30.276 +    else if (stop <= pos)
  30.277 +      find_command(pos, middle_index + 1, array_stop)
  30.278 +    else error("impossible")
  30.279 +  }
  30.280 +}
    31.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.2 +++ b/src/Tools/jEdit/src/proofdocument/prover.scala	Tue Dec 08 14:49:01 2009 +0100
    31.3 @@ -0,0 +1,175 @@
    31.4 +/*
    31.5 + * Higher-level prover communication: interactive document model
    31.6 + *
    31.7 + * @author Johannes Hölzl, TU Munich
    31.8 + * @author Fabian Immler, TU Munich
    31.9 + * @author Makarius
   31.10 + */
   31.11 +
   31.12 +package isabelle.prover
   31.13 +
   31.14 +
   31.15 +import scala.actors.Actor, Actor._
   31.16 +
   31.17 +import javax.swing.JTextArea
   31.18 +
   31.19 +import isabelle.jedit.Isabelle
   31.20 +import isabelle.proofdocument.{ProofDocument, Change, Token}
   31.21 +
   31.22 +
   31.23 +class Prover(system: Isabelle_System, logic: String)
   31.24 +{
   31.25 +  /* incoming messages */
   31.26 +
   31.27 +  private var prover_ready = false
   31.28 +
   31.29 +  private val receiver = new Actor {
   31.30 +    def act() {
   31.31 +      loop {
   31.32 +        react {
   31.33 +          case result: Isabelle_Process.Result => handle_result(result)
   31.34 +          case change: Change if prover_ready => handle_change(change)
   31.35 +          case bad if prover_ready => System.err.println("prover: ignoring bad message " + bad)
   31.36 +        }
   31.37 +      }
   31.38 +    }
   31.39 +  }
   31.40 +
   31.41 +  def input(change: Change) { receiver ! change }
   31.42 +
   31.43 +
   31.44 +  /* outgoing messages */
   31.45 +
   31.46 +  val command_change = new Event_Bus[Command]
   31.47 +  val document_change = new Event_Bus[ProofDocument]
   31.48 +
   31.49 +
   31.50 +  /* prover process */
   31.51 +
   31.52 +  private val process =
   31.53 +    new Isabelle_Process(system, receiver, "-m", "xsymbols", logic) with Isar_Document
   31.54 +
   31.55 +
   31.56 +  /* outer syntax keywords and completion */
   31.57 +
   31.58 +  @volatile private var _command_decls = Map[String, String]()
   31.59 +  def command_decls() = _command_decls
   31.60 +
   31.61 +  @volatile private var _keyword_decls = Set[String]()
   31.62 +  def keyword_decls() = _keyword_decls
   31.63 +
   31.64 +  @volatile private var _completion = Isabelle.completion
   31.65 +  def completion() = _completion
   31.66 +
   31.67 +
   31.68 +  /* document state information */
   31.69 +
   31.70 +  @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
   31.71 +  @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
   31.72 +  val document_0 =
   31.73 +    ProofDocument.empty.
   31.74 +    set_command_keyword((s: String) => command_decls().contains(s))
   31.75 +  @volatile private var document_versions = List(document_0)
   31.76 +
   31.77 +  def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
   31.78 +  def document(id: Isar_Document.Document_ID): Option[ProofDocument] =
   31.79 +    document_versions.find(_.id == id)
   31.80 +
   31.81 +
   31.82 +  /* prover results */
   31.83 +
   31.84 +  val output_text_view = new JTextArea    // FIXME separate jEdit component
   31.85 +
   31.86 +  private def handle_result(result: Isabelle_Process.Result)
   31.87 +  {
   31.88 +    // FIXME separate jEdit component
   31.89 +    Swing_Thread.later { output_text_view.append(result.toString + "\n") }
   31.90 +
   31.91 +    val message = Isabelle_Process.parse_message(system, result)
   31.92 +
   31.93 +    val state =
   31.94 +      Position.id_of(result.props) match {
   31.95 +        case None => None
   31.96 +        case Some(id) => commands.get(id) orElse states.get(id) orElse None
   31.97 +      }
   31.98 +    if (state.isDefined) state.get ! (this, message)
   31.99 +    else if (result.kind == Isabelle_Process.Kind.STATUS) {
  31.100 +      //{{{ global status message
  31.101 +      message match {
  31.102 +        case XML.Elem(Markup.MESSAGE, _, elems) =>
  31.103 +          for (elem <- elems) {
  31.104 +            elem match {
  31.105 +              // document edits
  31.106 +              case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
  31.107 +                document_versions.find(_.id == doc_id) match {
  31.108 +                  case Some(doc) =>
  31.109 +                    for {
  31.110 +                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
  31.111 +                      <- edits }
  31.112 +                    {
  31.113 +                      commands.get(cmd_id) match {
  31.114 +                        case Some(cmd) =>
  31.115 +                          val state = new Command_State(cmd)
  31.116 +                          states += (state_id -> state)
  31.117 +                          doc.states += (cmd -> state)
  31.118 +                          command_change.event(cmd)   // FIXME really!?
  31.119 +                        case None =>
  31.120 +                      }
  31.121 +                    }
  31.122 +                  case None =>
  31.123 +                }
  31.124 +
  31.125 +              // command and keyword declarations
  31.126 +              case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
  31.127 +                _command_decls += (name -> kind)
  31.128 +                _completion += name
  31.129 +              case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
  31.130 +                _keyword_decls += name
  31.131 +                _completion += name
  31.132 +
  31.133 +              // process ready (after initialization)
  31.134 +              case XML.Elem(Markup.READY, _, _) => prover_ready = true
  31.135 +
  31.136 +              case _ =>
  31.137 +            }
  31.138 +          }
  31.139 +        case _ =>
  31.140 +      }
  31.141 +      //}}}
  31.142 +    }
  31.143 +  }
  31.144 +
  31.145 +
  31.146 +  /* document changes */
  31.147 +
  31.148 +  def begin_document(path: String) {
  31.149 +    process.begin_document(document_0.id, path)
  31.150 +  }
  31.151 +
  31.152 +  def handle_change(change: Change) {
  31.153 +    val old = document(change.parent.get.id).get
  31.154 +    val (doc, changes) = old.text_changed(change)
  31.155 +    document_versions ::= doc
  31.156 +
  31.157 +    val id_changes = changes map { case (c1, c2) =>
  31.158 +        (c1.map(_.id).getOrElse(document_0.id),
  31.159 +         c2 match {
  31.160 +            case None => None
  31.161 +            case Some(command) =>
  31.162 +              commands += (command.id -> command)
  31.163 +              process.define_command(command.id, system.symbols.encode(command.content))
  31.164 +              Some(command.id)
  31.165 +          })
  31.166 +    }
  31.167 +    process.edit_document(old.id, doc.id, id_changes)
  31.168 +
  31.169 +    document_change.event(doc)
  31.170 +  }
  31.171 +
  31.172 +
  31.173 +  /* main controls */
  31.174 +
  31.175 +  def start() { receiver.start() }
  31.176 +
  31.177 +  def stop() { process.kill() }
  31.178 +}
    32.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.2 +++ b/src/Tools/jEdit/src/proofdocument/state.scala	Tue Dec 08 14:49:01 2009 +0100
    32.3 @@ -0,0 +1,117 @@
    32.4 +/*
    32.5 + * Accumulating results from prover
    32.6 + *
    32.7 + * @author Fabian Immler, TU Munich
    32.8 + * @author Makarius
    32.9 + */
   32.10 +
   32.11 +package isabelle.prover
   32.12 +
   32.13 +
   32.14 +class State(
   32.15 +  val command: Command,
   32.16 +  val status: Command.Status.Value,
   32.17 +  rev_results: List[XML.Tree],
   32.18 +  val markup_root: Markup_Text)
   32.19 +{
   32.20 +  def this(command: Command) =
   32.21 +    this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
   32.22 +
   32.23 +
   32.24 +  /* content */
   32.25 +
   32.26 +  private def set_status(st: Command.Status.Value): State =
   32.27 +    new State(command, st, rev_results, markup_root)
   32.28 +
   32.29 +  private def add_result(res: XML.Tree): State =
   32.30 +    new State(command, status, res :: rev_results, markup_root)
   32.31 +
   32.32 +  private def add_markup(node: Markup_Tree): State =
   32.33 +    new State(command, status, rev_results, markup_root + node)
   32.34 +
   32.35 +  lazy val results = rev_results.reverse
   32.36 +
   32.37 +
   32.38 +  /* markup */
   32.39 +
   32.40 +  lazy val highlight: Markup_Text =
   32.41 +  {
   32.42 +    markup_root.filter(_.info match {
   32.43 +      case Command.HighlightInfo(_) => true
   32.44 +      case _ => false
   32.45 +    })
   32.46 +  }
   32.47 +
   32.48 +  private lazy val types: List[Markup_Node] =
   32.49 +    markup_root.filter(_.info match {
   32.50 +      case Command.TypeInfo(_) => true
   32.51 +      case _ => false }).flatten
   32.52 +
   32.53 +  def type_at(pos: Int): Option[String] =
   32.54 +  {
   32.55 +    types.find(t => t.start <= pos && pos < t.stop) match {
   32.56 +      case Some(t) =>
   32.57 +        t.info match {
   32.58 +          case Command.TypeInfo(ty) => Some(command.content(t.start, t.stop) + ": " + ty)
   32.59 +          case _ => None
   32.60 +        }
   32.61 +      case None => None
   32.62 +    }
   32.63 +  }
   32.64 +
   32.65 +  private lazy val refs: List[Markup_Node] =
   32.66 +    markup_root.filter(_.info match {
   32.67 +      case Command.RefInfo(_, _, _, _) => true
   32.68 +      case _ => false }).flatten
   32.69 +
   32.70 +  def ref_at(pos: Int): Option[Markup_Node] =
   32.71 +    refs.find(t => t.start <= pos && pos < t.stop)
   32.72 +
   32.73 +
   32.74 +  /* message dispatch */
   32.75 +
   32.76 +  def + (prover: Prover, message: XML.Tree): State =
   32.77 +  {
   32.78 +    val changed: State =
   32.79 +      message match {
   32.80 +        case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
   32.81 +          (this /: elems)((state, elem) =>
   32.82 +            elem match {
   32.83 +              case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
   32.84 +              case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
   32.85 +              case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
   32.86 +              case XML.Elem(kind, atts, body) =>
   32.87 +                val (begin, end) = Position.offsets_of(atts)
   32.88 +                if (begin.isEmpty || end.isEmpty) state
   32.89 +                else if (kind == Markup.ML_TYPING) {
   32.90 +                  val info = body.first.asInstanceOf[XML.Text].content   // FIXME proper match!?
   32.91 +                  state.add_markup(
   32.92 +                    command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
   32.93 +                }
   32.94 +                else if (kind == Markup.ML_REF) {
   32.95 +                  body match {
   32.96 +                    case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
   32.97 +                      state.add_markup(command.markup_node(
   32.98 +                        begin.get - 1, end.get - 1,
   32.99 +                        Command.RefInfo(
  32.100 +                          Position.file_of(atts),
  32.101 +                          Position.line_of(atts),
  32.102 +                          Position.id_of(atts),
  32.103 +                          Position.offset_of(atts))))
  32.104 +                    case _ => state
  32.105 +                  }
  32.106 +                }
  32.107 +                else {
  32.108 +                  state.add_markup(
  32.109 +                    command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
  32.110 +                }
  32.111 +              case _ =>
  32.112 +                System.err.println("ignored status report: " + elem)
  32.113 +                state
  32.114 +            })
  32.115 +        case _ => add_result(message)
  32.116 +      }
  32.117 +    if (!(this eq changed)) prover.command_change.event(command)
  32.118 +    changed
  32.119 +  }
  32.120 +}
    33.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.2 +++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala	Tue Dec 08 14:49:01 2009 +0100
    33.3 @@ -0,0 +1,327 @@
    33.4 +/*
    33.5 + * jEdit text area as document text source
    33.6 + *
    33.7 + * @author Fabian Immler, TU Munich
    33.8 + * @author Johannes Hölzl, TU Munich
    33.9 + * @author Makarius
   33.10 + */
   33.11 +
   33.12 +package isabelle.jedit
   33.13 +
   33.14 +import scala.actors.Actor, Actor._
   33.15 +import scala.collection.mutable
   33.16 +
   33.17 +import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove}
   33.18 +import isabelle.prover.{Prover, Command}
   33.19 +
   33.20 +import java.awt.{Color, Graphics2D}
   33.21 +import javax.swing.event.{CaretListener, CaretEvent}
   33.22 +
   33.23 +import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
   33.24 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
   33.25 +import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
   33.26 +
   33.27 +
   33.28 +object TheoryView
   33.29 +{
   33.30 +  def choose_color(command: Command, doc: ProofDocument): Color =
   33.31 +  {
   33.32 +    command.status(doc) match {
   33.33 +      case Command.Status.UNPROCESSED => new Color(255, 228, 225)
   33.34 +      case Command.Status.FINISHED => new Color(234, 248, 255)
   33.35 +      case Command.Status.FAILED => new Color(255, 106, 106)
   33.36 +      case _ => Color.red
   33.37 +    }
   33.38 +  }
   33.39 +}
   33.40 +
   33.41 +
   33.42 +class TheoryView(text_area: JEditTextArea)
   33.43 +{
   33.44 +  private val buffer = text_area.getBuffer
   33.45 +
   33.46 +
   33.47 +  /* prover setup */
   33.48 +
   33.49 +  val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic())
   33.50 +
   33.51 +  prover.command_change += ((command: Command) =>
   33.52 +    if (current_document().commands.contains(command))
   33.53 +      Swing_Thread.later {
   33.54 +        // FIXME proper handling of buffer vs. text areas
   33.55 +        // repaint if buffer is active
   33.56 +        if (text_area.getBuffer == buffer) {
   33.57 +          update_syntax(command)
   33.58 +          invalidate_line(command)
   33.59 +          overview.repaint()
   33.60 +        }
   33.61 +      })
   33.62 +
   33.63 +
   33.64 +  /* changes vs. edits */
   33.65 +
   33.66 +  private val change_0 = new Change(prover.document_0.id, None, Nil)
   33.67 +  private var _changes = List(change_0)   // owned by Swing/AWT thread
   33.68 +  def changes = _changes
   33.69 +  private var current_change = change_0
   33.70 +
   33.71 +  private val edits = new mutable.ListBuffer[Edit]   // owned by Swing thread
   33.72 +
   33.73 +  private val edits_delay = Swing_Thread.delay_last(300) {
   33.74 +    if (!edits.isEmpty) {
   33.75 +      val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList)
   33.76 +      _changes ::= change
   33.77 +      prover.input(change)
   33.78 +      current_change = change
   33.79 +      edits.clear
   33.80 +    }
   33.81 +  }
   33.82 +
   33.83 +
   33.84 +  /* buffer_listener */
   33.85 +
   33.86 +  private val buffer_listener = new BufferListener {
   33.87 +    override def preContentInserted(buffer: JEditBuffer,
   33.88 +      start_line: Int, offset: Int, num_lines: Int, length: Int)
   33.89 +    {
   33.90 +      edits += Insert(offset, buffer.getText(offset, length))
   33.91 +      edits_delay()
   33.92 +    }
   33.93 +
   33.94 +    override def preContentRemoved(buffer: JEditBuffer,
   33.95 +      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
   33.96 +    {
   33.97 +      edits += Remove(start, buffer.getText(start, removed_length))
   33.98 +      edits_delay()
   33.99 +    }
  33.100 +
  33.101 +    override def contentInserted(buffer: JEditBuffer,
  33.102 +      start_line: Int, offset: Int, num_lines: Int, length: Int) { }
  33.103 +
  33.104 +    override def contentRemoved(buffer: JEditBuffer,
  33.105 +      start_line: Int, offset: Int, num_lines: Int, length: Int) { }
  33.106 +
  33.107 +    override def bufferLoaded(buffer: JEditBuffer) { }
  33.108 +    override def foldHandlerChanged(buffer: JEditBuffer) { }
  33.109 +    override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
  33.110 +    override def transactionComplete(buffer: JEditBuffer) { }
  33.111 +  }
  33.112 +
  33.113 +
  33.114 +  /* text_area_extension */
  33.115 +
  33.116 +  private val text_area_extension = new TextAreaExtension {
  33.117 +    override def paintValidLine(gfx: Graphics2D,
  33.118 +      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
  33.119 +    {
  33.120 +      val document = current_document()
  33.121 +      def from_current(pos: Int) = TheoryView.this.from_current(document, pos)
  33.122 +      def to_current(pos: Int) = TheoryView.this.to_current(document, pos)
  33.123 +      val saved_color = gfx.getColor
  33.124 +
  33.125 +      val metrics = text_area.getPainter.getFontMetrics
  33.126 +
  33.127 +      // encolor phase
  33.128 +      var cmd = document.command_at(from_current(start))
  33.129 +      while (cmd.isDefined && cmd.get.start(document) < end) {
  33.130 +        val e = cmd.get
  33.131 +        val begin = start max to_current(e.start(document))
  33.132 +        val finish = (end - 1) min to_current(e.stop(document))
  33.133 +        encolor(gfx, y, metrics.getHeight, begin, finish,
  33.134 +          TheoryView.choose_color(e, document), true)
  33.135 +        cmd = document.commands.next(e)
  33.136 +      }
  33.137 +
  33.138 +      gfx.setColor(saved_color)
  33.139 +    }
  33.140 +
  33.141 +    override def getToolTipText(x: Int, y: Int): String =
  33.142 +    {
  33.143 +      val document = current_document()
  33.144 +      val offset = from_current(document, text_area.xyToOffset(x, y))
  33.145 +      document.command_at(offset) match {
  33.146 +        case Some(cmd) =>
  33.147 +          document.token_start(cmd.tokens.first)
  33.148 +          cmd.type_at(document, offset - cmd.start(document)).getOrElse(null)
  33.149 +        case None => null
  33.150 +      }
  33.151 +    }
  33.152 +  }
  33.153 +
  33.154 +
  33.155 +  /* activation */
  33.156 +
  33.157 +  private val overview = new Document_Overview(prover, text_area, to_current)
  33.158 +
  33.159 +  private val selected_state_controller = new CaretListener {
  33.160 +    override def caretUpdate(e: CaretEvent) {
  33.161 +      val doc = current_document()
  33.162 +      doc.command_at(e.getDot) match {
  33.163 +        case Some(cmd)
  33.164 +          if (doc.token_start(cmd.tokens.first) <= e.getDot &&
  33.165 +            Isabelle.plugin.selected_state != cmd) =>
  33.166 +          Isabelle.plugin.selected_state = cmd
  33.167 +        case _ =>
  33.168 +      }
  33.169 +    }
  33.170 +  }
  33.171 +
  33.172 +  def activate() {
  33.173 +    text_area.addCaretListener(selected_state_controller)
  33.174 +    text_area.addLeftOfScrollBar(overview)
  33.175 +    text_area.getPainter.
  33.176 +      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
  33.177 +    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
  33.178 +    buffer.addBufferListener(buffer_listener)
  33.179 +
  33.180 +    val dockable =
  33.181 +      text_area.getView.getDockableWindowManager.getDockable("isabelle-output")
  33.182 +    if (dockable != null) {
  33.183 +      val output_dockable = dockable.asInstanceOf[OutputDockable]
  33.184 +      val output_text_view = prover.output_text_view
  33.185 +      output_dockable.set_text(output_text_view)
  33.186 +    }
  33.187 +
  33.188 +    buffer.propertiesChanged()
  33.189 +  }
  33.190 +
  33.191 +  def deactivate() {
  33.192 +    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
  33.193 +    buffer.removeBufferListener(buffer_listener)
  33.194 +    text_area.getPainter.removeExtension(text_area_extension)
  33.195 +    text_area.removeLeftOfScrollBar(overview)
  33.196 +    text_area.removeCaretListener(selected_state_controller)
  33.197 +  }
  33.198 +
  33.199 +
  33.200 +  /* history of changes */
  33.201 +
  33.202 +  private def doc_or_pred(c: Change): ProofDocument =
  33.203 +    prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
  33.204 +
  33.205 +  def current_document() = doc_or_pred(current_change)
  33.206 +
  33.207 +
  33.208 +  /* update to desired version */
  33.209 +
  33.210 +  def set_version(goal: Change) {
  33.211 +    // changes in buffer must be ignored
  33.212 +    buffer.removeBufferListener(buffer_listener)
  33.213 +
  33.214 +    def apply(change: Change): Unit = change.edits.foreach {
  33.215 +      case Insert(start, text) => buffer.insert(start, text)
  33.216 +      case Remove(start, text) => buffer.remove(start, text.length)
  33.217 +    }
  33.218 +
  33.219 +    def unapply(change: Change): Unit = change.edits.reverse.foreach {
  33.220 +      case Insert(start, text) => buffer.remove(start, text.length)
  33.221 +      case Remove(start, text) => buffer.insert(start, text)
  33.222 +    }
  33.223 +
  33.224 +    // undo/redo changes
  33.225 +    val ancs_current = current_change.ancestors
  33.226 +    val ancs_goal = goal.ancestors
  33.227 +    val paired = ancs_current.reverse zip ancs_goal.reverse
  33.228 +    def last_common[A](xs: List[(A, A)]): Option[A] = {
  33.229 +      xs match {
  33.230 +        case (x, y) :: xs =>
  33.231 +          if (x == y)
  33.232 +            xs match {
  33.233 +              case (a, b) :: ys =>
  33.234 +                if (a == b) last_common(xs)
  33.235 +                else Some(x)
  33.236 +              case _ => Some(x)
  33.237 +            }
  33.238 +          else None
  33.239 +        case _ => None
  33.240 +      }
  33.241 +    }
  33.242 +    val common_anc = last_common(paired).get
  33.243 +
  33.244 +    ancs_current.takeWhile(_ != common_anc) map unapply
  33.245 +    ancs_goal.takeWhile(_ != common_anc).reverse map apply
  33.246 +
  33.247 +    current_change = goal
  33.248 +    // invoke repaint
  33.249 +    buffer.propertiesChanged()
  33.250 +    invalidate_all()
  33.251 +    overview.repaint()
  33.252 +
  33.253 +    // track changes in buffer
  33.254 +    buffer.addBufferListener(buffer_listener)
  33.255 +  }
  33.256 +
  33.257 +
  33.258 +  /* transforming offsets */
  33.259 +
  33.260 +  private def changes_from(doc: ProofDocument): List[Edit] =
  33.261 +    List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
  33.262 +      edits.toList
  33.263 +
  33.264 +  def from_current(doc: ProofDocument, offset: Int): Int =
  33.265 +    (offset /: changes_from(doc).reverse) ((i, change) => change before i)
  33.266 +
  33.267 +  def to_current(doc: ProofDocument, offset: Int): Int =
  33.268 +    (offset /: changes_from(doc)) ((i, change) => change after i)
  33.269 +
  33.270 +
  33.271 +  private def lines_of_command(cmd: Command) =
  33.272 +  {
  33.273 +    val document = current_document()
  33.274 +    (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
  33.275 +     buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
  33.276 +  }
  33.277 +
  33.278 +
  33.279 +  /* (re)painting */
  33.280 +
  33.281 +  private val update_delay = Swing_Thread.delay_first(500) { buffer.propertiesChanged() }
  33.282 +
  33.283 +  private def update_syntax(cmd: Command) {
  33.284 +    val (line1, line2) = lines_of_command(cmd)
  33.285 +    if (line2 >= text_area.getFirstLine &&
  33.286 +      line1 <= text_area.getFirstLine + text_area.getVisibleLines)
  33.287 +        update_delay()
  33.288 +  }
  33.289 +
  33.290 +  private def invalidate_line(cmd: Command) =
  33.291 +  {
  33.292 +    val (start, stop) = lines_of_command(cmd)
  33.293 +    text_area.invalidateLineRange(start, stop)
  33.294 +
  33.295 +    if (Isabelle.plugin.selected_state == cmd)
  33.296 +      Isabelle.plugin.selected_state = cmd  // update State view
  33.297 +  }
  33.298 +
  33.299 +  private def invalidate_all() =
  33.300 +    text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
  33.301 +      text_area.getLastPhysicalLine)
  33.302 +
  33.303 +  private def encolor(gfx: Graphics2D,
  33.304 +    y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
  33.305 +  {
  33.306 +    val start = text_area.offsetToXY(begin)
  33.307 +    val stop =
  33.308 +      if (finish < buffer.getLength) text_area.offsetToXY(finish)
  33.309 +      else {
  33.310 +        val p = text_area.offsetToXY(finish - 1)
  33.311 +        val metrics = text_area.getPainter.getFontMetrics
  33.312 +        p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
  33.313 +        p
  33.314 +      }
  33.315 +
  33.316 +    if (start != null && stop != null) {
  33.317 +      gfx.setColor(color)
  33.318 +      if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
  33.319 +      else gfx.drawRect(start.x, y, stop.x - start.x, height)
  33.320 +    }
  33.321 +  }
  33.322 +
  33.323 +
  33.324 +  /* init */
  33.325 +
  33.326 +  prover.start()
  33.327 +
  33.328 +  edits += Insert(0, buffer.getText(0, buffer.getLength))
  33.329 +  edits_delay()
  33.330 +}
    34.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    34.2 +++ b/src/Tools/jEdit/src/proofdocument/token.scala	Tue Dec 08 14:49:01 2009 +0100
    34.3 @@ -0,0 +1,42 @@
    34.4 +/*
    34.5 + * Document tokens as text ranges
    34.6 + *
    34.7 + * @author Johannes Hölzl, TU Munich
    34.8 + * @author Fabian Immler, TU Munich
    34.9 + */
   34.10 +
   34.11 +package isabelle.proofdocument
   34.12 +
   34.13 +
   34.14 +import isabelle.prover.Command
   34.15 +
   34.16 +
   34.17 +object Token {
   34.18 +  object Kind extends Enumeration
   34.19 +  {
   34.20 +    val COMMAND_START = Value("COMMAND_START")
   34.21 +    val COMMENT = Value("COMMENT")
   34.22 +    val OTHER = Value("OTHER")
   34.23 +  }
   34.24 +
   34.25 +  def string_from_tokens(tokens: List[Token], starts: Token => Int): String = {
   34.26 +    def stop(t: Token) = starts(t) + t.length
   34.27 +    tokens match {
   34.28 +      case Nil => ""
   34.29 +      case tok :: toks =>
   34.30 +        val (res, _) = toks.foldLeft(tok.content, stop(tok))((a, token) =>
   34.31 +          (a._1 + " " * (starts(token) - a._2) + token.content, stop(token)))
   34.32 +        res
   34.33 +    }
   34.34 +  }
   34.35 +
   34.36 +}
   34.37 +
   34.38 +class Token(
   34.39 +  val content: String,
   34.40 +  val kind: Token.Kind.Value)
   34.41 +{
   34.42 +  override def toString = content
   34.43 +  val length = content.length
   34.44 +  val is_start = kind == Token.Kind.COMMAND_START || kind == Token.Kind.COMMENT
   34.45 +}
    35.1 --- a/src/Tools/jEdit/src/prover/Command.scala	Tue Dec 08 14:29:29 2009 +0100
    35.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    35.3 @@ -1,124 +0,0 @@
    35.4 -/*
    35.5 - * Prover commands with semantic state
    35.6 - *
    35.7 - * @author Johannes Hölzl, TU Munich
    35.8 - * @author Fabian Immler, TU Munich
    35.9 - */
   35.10 -
   35.11 -package isabelle.prover
   35.12 -
   35.13 -
   35.14 -import scala.actors.Actor, Actor._
   35.15 -
   35.16 -import scala.collection.mutable
   35.17 -
   35.18 -import isabelle.proofdocument.{Token, ProofDocument}
   35.19 -import isabelle.jedit.{Isabelle, Plugin}
   35.20 -import isabelle.XML
   35.21 -
   35.22 -
   35.23 -trait Accumulator extends Actor
   35.24 -{
   35.25 -  start() // start actor
   35.26 -
   35.27 -  protected var _state: State
   35.28 -  def state = _state
   35.29 -
   35.30 -  override def act() {
   35.31 -    loop {
   35.32 -      react {
   35.33 -        case (prover: Prover, message: XML.Tree) => _state = _state.+(prover, message)
   35.34 -        case bad => System.err.println("prover: ignoring bad message " + bad)
   35.35 -      }
   35.36 -    }
   35.37 -  }
   35.38 -}
   35.39 -
   35.40 -
   35.41 -object Command
   35.42 -{
   35.43 -  object Status extends Enumeration
   35.44 -  {
   35.45 -    val UNPROCESSED = Value("UNPROCESSED")
   35.46 -    val FINISHED = Value("FINISHED")
   35.47 -    val FAILED = Value("FAILED")
   35.48 -  }
   35.49 -
   35.50 -  case class HighlightInfo(highlight: String) { override def toString = highlight }
   35.51 -  case class TypeInfo(ty: String)
   35.52 -  case class RefInfo(file: Option[String], line: Option[Int],
   35.53 -    command_id: Option[String], offset: Option[Int])
   35.54 -}
   35.55 -
   35.56 -
   35.57 -class Command(
   35.58 -    val tokens: List[Token],
   35.59 -    val starts: Map[Token, Int]) extends Accumulator
   35.60 -{
   35.61 -  require(!tokens.isEmpty)
   35.62 -
   35.63 -  val id = Isabelle.system.id()
   35.64 -  override def hashCode = id.hashCode
   35.65 -
   35.66 -
   35.67 -  /* content */
   35.68 -
   35.69 -  override def toString = name
   35.70 -
   35.71 -  val name = tokens.head.content
   35.72 -  val content: String = Token.string_from_tokens(tokens, starts)
   35.73 -  def content(i: Int, j: Int): String = content.substring(i, j)
   35.74 -  val symbol_index = new Symbol.Index(content)
   35.75 -
   35.76 -  def start(doc: ProofDocument) = doc.token_start(tokens.first)
   35.77 -  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
   35.78 -
   35.79 -  def contains(p: Token) = tokens.contains(p)
   35.80 -
   35.81 -  protected override var _state = new State(this)
   35.82 -
   35.83 -
   35.84 -  /* markup */
   35.85 -
   35.86 -  lazy val empty_markup = new Markup_Text(Nil, content)
   35.87 -
   35.88 -  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
   35.89 -  {
   35.90 -    val start = symbol_index.decode(begin)
   35.91 -    val stop = symbol_index.decode(end)
   35.92 -    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
   35.93 -  }
   35.94 -
   35.95 -
   35.96 -  /* results, markup, ... */
   35.97 -
   35.98 -  private val empty_cmd_state = new Command_State(this)
   35.99 -  private def cmd_state(doc: ProofDocument) =
  35.100 -    doc.states.getOrElse(this, empty_cmd_state)
  35.101 -
  35.102 -  def status(doc: ProofDocument) = cmd_state(doc).state.status
  35.103 -  def results(doc: ProofDocument) = cmd_state(doc).results
  35.104 -  def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
  35.105 -  def highlight(doc: ProofDocument) = cmd_state(doc).highlight
  35.106 -  def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
  35.107 -  def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
  35.108 -}
  35.109 -
  35.110 -
  35.111 -class Command_State(val command: Command) extends Accumulator
  35.112 -{
  35.113 -  protected override var _state = new State(command)
  35.114 -
  35.115 -  def results: List[XML.Tree] =
  35.116 -    command.state.results ::: state.results
  35.117 -
  35.118 -  def markup_root: Markup_Text =
  35.119 -    (command.state.markup_root /: state.markup_root.markup)(_ + _)
  35.120 -
  35.121 -  def type_at(pos: Int): Option[String] = state.type_at(pos)
  35.122 -
  35.123 -  def ref_at(pos: Int): Option[Markup_Node] = state.ref_at(pos)
  35.124 -
  35.125 -  def highlight: Markup_Text =
  35.126 -    (command.state.highlight /: state.highlight.markup)(_ + _)
  35.127 -}
  35.128 \ No newline at end of file
    36.1 --- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Tue Dec 08 14:29:29 2009 +0100
    36.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    36.3 @@ -1,111 +0,0 @@
    36.4 -/*
    36.5 - * Document markup nodes, with connection to Swing tree model
    36.6 - *
    36.7 - * @author Fabian Immler, TU Munich
    36.8 - */
    36.9 -
   36.10 -package isabelle.prover
   36.11 -
   36.12 -
   36.13 -import javax.swing.tree.DefaultMutableTreeNode
   36.14 -
   36.15 -import isabelle.proofdocument.ProofDocument
   36.16 -
   36.17 -
   36.18 -class Markup_Node(val start: Int, val stop: Int, val info: Any)
   36.19 -{
   36.20 -  def fits_into(that: Markup_Node): Boolean =
   36.21 -    that.start <= this.start && this.stop <= that.stop
   36.22 -}
   36.23 -
   36.24 -
   36.25 -class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
   36.26 -{
   36.27 -  def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
   36.28 -
   36.29 -  private def add(branch: Markup_Tree) =   // FIXME avoid sort
   36.30 -    set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
   36.31 -
   36.32 -  private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
   36.33 -
   36.34 -  def + (new_tree: Markup_Tree): Markup_Tree =
   36.35 -  {
   36.36 -    val new_node = new_tree.node
   36.37 -    if (new_node fits_into node) {
   36.38 -      var inserted = false
   36.39 -      val new_branches =
   36.40 -        branches.map(branch =>
   36.41 -          if ((new_node fits_into branch.node) && !inserted) {
   36.42 -            inserted = true
   36.43 -            branch + new_tree
   36.44 -          }
   36.45 -          else branch)
   36.46 -      if (!inserted) {
   36.47 -        // new_tree did not fit into children of this
   36.48 -        // -> insert between this and its branches
   36.49 -        val fitting = branches filter(_.node fits_into new_node)
   36.50 -        (this remove fitting) add ((new_tree /: fitting)(_ + _))
   36.51 -      }
   36.52 -      else set_branches(new_branches)
   36.53 -    }
   36.54 -    else {
   36.55 -      System.err.println("ignored nonfitting markup: " + new_node)
   36.56 -      this
   36.57 -    }
   36.58 -  }
   36.59 -
   36.60 -  def flatten: List[Markup_Node] =
   36.61 -  {
   36.62 -    var next_x = node.start
   36.63 -    if (branches.isEmpty) List(this.node)
   36.64 -    else {
   36.65 -      val filled_gaps =
   36.66 -        for {
   36.67 -          child <- branches
   36.68 -          markups =
   36.69 -            if (next_x < child.node.start)
   36.70 -              new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
   36.71 -            else child.flatten
   36.72 -          update = (next_x = child.node.stop)
   36.73 -          markup <- markups
   36.74 -        } yield markup
   36.75 -      if (next_x < node.stop)
   36.76 -        filled_gaps + new Markup_Node(next_x, node.stop, node.info)
   36.77 -      else filled_gaps
   36.78 -    }
   36.79 -  }
   36.80 -}
   36.81 -
   36.82 -
   36.83 -class Markup_Text(val markup: List[Markup_Tree], val content: String)
   36.84 -{
   36.85 -  private lazy val root =
   36.86 -    new Markup_Tree(new Markup_Node(0, content.length, None), markup)
   36.87 -
   36.88 -  def + (new_tree: Markup_Tree): Markup_Text =
   36.89 -    new Markup_Text((root + new_tree).branches, content)
   36.90 -
   36.91 -  def filter(pred: Markup_Node => Boolean): Markup_Text =
   36.92 -  {
   36.93 -    def filt(tree: Markup_Tree): List[Markup_Tree] =
   36.94 -    {
   36.95 -      val branches = tree.branches.flatMap(filt(_))
   36.96 -      if (pred(tree.node)) List(tree.set_branches(branches))
   36.97 -      else branches
   36.98 -    }
   36.99 -    new Markup_Text(markup.flatMap(filt(_)), content)
  36.100 -  }
  36.101 -
  36.102 -  def flatten: List[Markup_Node] = markup.flatten(_.flatten)
  36.103 -
  36.104 -  def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
  36.105 -  {
  36.106 -    def swing(tree: Markup_Tree): DefaultMutableTreeNode =
  36.107 -    {
  36.108 -      val node = swing_node(tree.node)
  36.109 -      tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
  36.110 -      node
  36.111 -    }
  36.112 -    swing(root)
  36.113 -  }
  36.114 -}
    37.1 --- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Dec 08 14:29:29 2009 +0100
    37.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    37.3 @@ -1,175 +0,0 @@
    37.4 -/*
    37.5 - * Higher-level prover communication: interactive document model
    37.6 - *
    37.7 - * @author Johannes Hölzl, TU Munich
    37.8 - * @author Fabian Immler, TU Munich
    37.9 - * @author Makarius
   37.10 - */
   37.11 -
   37.12 -package isabelle.prover
   37.13 -
   37.14 -
   37.15 -import scala.actors.Actor, Actor._
   37.16 -
   37.17 -import javax.swing.JTextArea
   37.18 -
   37.19 -import isabelle.jedit.Isabelle
   37.20 -import isabelle.proofdocument.{ProofDocument, Change, Token}
   37.21 -
   37.22 -
   37.23 -class Prover(system: Isabelle_System, logic: String)
   37.24 -{
   37.25 -  /* incoming messages */
   37.26 -
   37.27 -  private var prover_ready = false
   37.28 -
   37.29 -  private val receiver = new Actor {
   37.30 -    def act() {
   37.31 -      loop {
   37.32 -        react {
   37.33 -          case result: Isabelle_Process.Result => handle_result(result)
   37.34 -          case change: Change if prover_ready => handle_change(change)
   37.35 -          case bad if prover_ready => System.err.println("prover: ignoring bad message " + bad)
   37.36 -        }
   37.37 -      }
   37.38 -    }
   37.39 -  }
   37.40 -
   37.41 -  def input(change: Change) { receiver ! change }
   37.42 -
   37.43 -
   37.44 -  /* outgoing messages */
   37.45 -
   37.46 -  val command_change = new Event_Bus[Command]
   37.47 -  val document_change = new Event_Bus[ProofDocument]
   37.48 -
   37.49 -
   37.50 -  /* prover process */
   37.51 -
   37.52 -  private val process =
   37.53 -    new Isabelle_Process(system, receiver, "-m", "xsymbols", logic) with Isar_Document
   37.54 -
   37.55 -
   37.56 -  /* outer syntax keywords and completion */
   37.57 -
   37.58 -  @volatile private var _command_decls = Map[String, String]()
   37.59 -  def command_decls() = _command_decls
   37.60 -
   37.61 -  @volatile private var _keyword_decls = Set[String]()
   37.62 -  def keyword_decls() = _keyword_decls
   37.63 -
   37.64 -  @volatile private var _completion = Isabelle.completion
   37.65 -  def completion() = _completion
   37.66 -
   37.67 -
   37.68 -  /* document state information */
   37.69 -
   37.70 -  @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
   37.71 -  @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
   37.72 -  val document_0 =
   37.73 -    ProofDocument.empty.
   37.74 -    set_command_keyword((s: String) => command_decls().contains(s))
   37.75 -  @volatile private var document_versions = List(document_0)
   37.76 -
   37.77 -  def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
   37.78 -  def document(id: Isar_Document.Document_ID): Option[ProofDocument] =
   37.79 -    document_versions.find(_.id == id)
   37.80 -
   37.81 -
   37.82 -  /* prover results */
   37.83 -
   37.84 -  val output_text_view = new JTextArea    // FIXME separate jEdit component
   37.85 -
   37.86 -  private def handle_result(result: Isabelle_Process.Result)
   37.87 -  {
   37.88 -    // FIXME separate jEdit component
   37.89 -    Swing_Thread.later { output_text_view.append(result.toString + "\n") }
   37.90 -
   37.91 -    val message = Isabelle_Process.parse_message(system, result)
   37.92 -
   37.93 -    val state =
   37.94 -      Position.id_of(result.props) match {
   37.95 -        case None => None
   37.96 -        case Some(id) => commands.get(id) orElse states.get(id) orElse None
   37.97 -      }
   37.98 -    if (state.isDefined) state.get ! (this, message)
   37.99 -    else if (result.kind == Isabelle_Process.Kind.STATUS) {
  37.100 -      //{{{ global status message
  37.101 -      message match {
  37.102 -        case XML.Elem(Markup.MESSAGE, _, elems) =>
  37.103 -          for (elem <- elems) {
  37.104 -            elem match {
  37.105 -              // document edits
  37.106 -              case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
  37.107 -                document_versions.find(_.id == doc_id) match {
  37.108 -                  case Some(doc) =>
  37.109 -                    for {
  37.110 -                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
  37.111 -                      <- edits }
  37.112 -                    {
  37.113 -                      commands.get(cmd_id) match {
  37.114 -                        case Some(cmd) =>
  37.115 -                          val state = new Command_State(cmd)
  37.116 -                          states += (state_id -> state)
  37.117 -                          doc.states += (cmd -> state)
  37.118 -                          command_change.event(cmd)   // FIXME really!?
  37.119 -                        case None =>
  37.120 -                      }
  37.121 -                    }
  37.122 -                  case None =>
  37.123 -                }
  37.124 -
  37.125 -              // command and keyword declarations
  37.126 -              case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
  37.127 -                _command_decls += (name -> kind)
  37.128 -                _completion += name
  37.129 -              case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
  37.130 -                _keyword_decls += name
  37.131 -                _completion += name
  37.132 -
  37.133 -              // process ready (after initialization)
  37.134 -              case XML.Elem(Markup.READY, _, _) => prover_ready = true
  37.135 -
  37.136 -              case _ =>
  37.137 -            }
  37.138 -          }
  37.139 -        case _ =>
  37.140 -      }
  37.141 -      //}}}
  37.142 -    }
  37.143 -  }
  37.144 -
  37.145 -
  37.146 -  /* document changes */
  37.147 -
  37.148 -  def begin_document(path: String) {
  37.149 -    process.begin_document(document_0.id, path)
  37.150 -  }
  37.151 -
  37.152 -  def handle_change(change: Change) {
  37.153 -    val old = document(change.parent.get.id).get
  37.154 -    val (doc, changes) = old.text_changed(change)
  37.155 -    document_versions ::= doc
  37.156 -
  37.157 -    val id_changes = changes map { case (c1, c2) =>
  37.158 -        (c1.map(_.id).getOrElse(document_0.id),
  37.159 -         c2 match {
  37.160 -            case None => None
  37.161 -            case Some(command) =>
  37.162 -              commands += (command.id -> command)
  37.163 -              process.define_command(command.id, system.symbols.encode(command.content))
  37.164 -              Some(command.id)
  37.165 -          })
  37.166 -    }
  37.167 -    process.edit_document(old.id, doc.id, id_changes)
  37.168 -
  37.169 -    document_change.event(doc)
  37.170 -  }
  37.171 -
  37.172 -
  37.173 -  /* main controls */
  37.174 -
  37.175 -  def start() { receiver.start() }
  37.176 -
  37.177 -  def stop() { process.kill() }
  37.178 -}
    38.1 --- a/src/Tools/jEdit/src/prover/State.scala	Tue Dec 08 14:29:29 2009 +0100
    38.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    38.3 @@ -1,117 +0,0 @@
    38.4 -/*
    38.5 - * Accumulating results from prover
    38.6 - *
    38.7 - * @author Fabian Immler, TU Munich
    38.8 - * @author Makarius
    38.9 - */
   38.10 -
   38.11 -package isabelle.prover
   38.12 -
   38.13 -
   38.14 -class State(
   38.15 -  val command: Command,
   38.16 -  val status: Command.Status.Value,
   38.17 -  rev_results: List[XML.Tree],
   38.18 -  val markup_root: Markup_Text)
   38.19 -{
   38.20 -  def this(command: Command) =
   38.21 -    this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
   38.22 -
   38.23 -
   38.24 -  /* content */
   38.25 -
   38.26 -  private def set_status(st: Command.Status.Value): State =
   38.27 -    new State(command, st, rev_results, markup_root)
   38.28 -
   38.29 -  private def add_result(res: XML.Tree): State =
   38.30 -    new State(command, status, res :: rev_results, markup_root)
   38.31 -
   38.32 -  private def add_markup(node: Markup_Tree): State =
   38.33 -    new State(command, status, rev_results, markup_root + node)
   38.34 -
   38.35 -  lazy val results = rev_results.reverse
   38.36 -
   38.37 -
   38.38 -  /* markup */
   38.39 -
   38.40 -  lazy val highlight: Markup_Text =
   38.41 -  {
   38.42 -    markup_root.filter(_.info match {
   38.43 -      case Command.HighlightInfo(_) => true
   38.44 -      case _ => false
   38.45 -    })
   38.46 -  }
   38.47 -
   38.48 -  private lazy val types: List[Markup_Node] =
   38.49 -    markup_root.filter(_.info match {
   38.50 -      case Command.TypeInfo(_) => true
   38.51 -      case _ => false }).flatten
   38.52 -
   38.53 -  def type_at(pos: Int): Option[String] =
   38.54 -  {
   38.55 -    types.find(t => t.start <= pos && pos < t.stop) match {
   38.56 -      case Some(t) =>
   38.57 -        t.info match {
   38.58 -          case Command.TypeInfo(ty) => Some(command.content(t.start, t.stop) + ": " + ty)
   38.59 -          case _ => None
   38.60 -        }
   38.61 -      case None => None
   38.62 -    }
   38.63 -  }
   38.64 -
   38.65 -  private lazy val refs: List[Markup_Node] =
   38.66 -    markup_root.filter(_.info match {
   38.67 -      case Command.RefInfo(_, _, _, _) => true
   38.68 -      case _ => false }).flatten
   38.69 -
   38.70 -  def ref_at(pos: Int): Option[Markup_Node] =
   38.71 -    refs.find(t => t.start <= pos && pos < t.stop)
   38.72 -
   38.73 -
   38.74 -  /* message dispatch */
   38.75 -
   38.76 -  def + (prover: Prover, message: XML.Tree): State =
   38.77 -  {
   38.78 -    val changed: State =
   38.79 -      message match {
   38.80 -        case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
   38.81 -          (this /: elems)((state, elem) =>
   38.82 -            elem match {
   38.83 -              case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
   38.84 -              case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
   38.85 -              case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
   38.86 -              case XML.Elem(kind, atts, body) =>
   38.87 -                val (begin, end) = Position.offsets_of(atts)
   38.88 -                if (begin.isEmpty || end.isEmpty) state
   38.89 -                else if (kind == Markup.ML_TYPING) {
   38.90 -                  val info = body.first.asInstanceOf[XML.Text].content   // FIXME proper match!?
   38.91 -                  state.add_markup(
   38.92 -                    command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
   38.93 -                }
   38.94 -                else if (kind == Markup.ML_REF) {
   38.95 -                  body match {
   38.96 -                    case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
   38.97 -                      state.add_markup(command.markup_node(
   38.98 -                        begin.get - 1, end.get - 1,
   38.99 -                        Command.RefInfo(
  38.100 -                          Position.file_of(atts),
  38.101 -                          Position.line_of(atts),
  38.102 -                          Position.id_of(atts),
  38.103 -                          Position.offset_of(atts))))
  38.104 -                    case _ => state
  38.105 -                  }
  38.106 -                }
  38.107 -                else {
  38.108 -                  state.add_markup(
  38.109 -                    command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
  38.110 -                }
  38.111 -              case _ =>
  38.112 -                System.err.println("ignored status report: " + elem)
  38.113 -                state
  38.114 -            })
  38.115 -        case _ => add_result(message)
  38.116 -      }
  38.117 -    if (!(this eq changed)) prover.command_change.event(command)
  38.118 -    changed
  38.119 -  }
  38.120 -}