misc modernization of names;
authorwenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34761 0ad6d8372f9d
misc modernization of names;
src/Tools/jEdit/dist-template/properties/jedit.props
src/Tools/jEdit/plugin/Isabelle.props
src/Tools/jEdit/plugin/actions.xml
src/Tools/jEdit/plugin/dockables.xml
src/Tools/jEdit/plugin/services.xml
src/Tools/jEdit/src/jedit/browse_version_dockable.scala
src/Tools/jEdit/src/jedit/document_overview.scala
src/Tools/jEdit/src/jedit/history_dockable.scala
src/Tools/jEdit/src/jedit/isabelle_encoding.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
src/Tools/jEdit/src/jedit/isabelle_options.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit/isabelle_token_marker.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/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
     1.1 --- a/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Dec 08 14:49:01 2009 +0100
     1.2 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Dec 08 16:30:20 2009 +0100
     1.3 @@ -170,9 +170,9 @@
     1.4  encodingDetectors=BOM XML-PI buffer-local-property
     1.5  fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
     1.6  firstTime=false
     1.7 -isabelle-browser.dock-position=bottom
     1.8 -isabelle-output.dock-position=bottom
     1.9 -isabelle-state.dock-position=bottom
    1.10 +isabelle-history.dock-position=bottom
    1.11 +isabelle-raw-output.dock-position=bottom
    1.12 +isabelle-results.dock-position=bottom
    1.13  isabelle.activate.shortcut=CS+ENTER
    1.14  mode.isabelle.sidekick.showStatusWindow.label=true
    1.15  sidekick-tree.dock-position=right
     2.1 --- a/src/Tools/jEdit/plugin/Isabelle.props	Tue Dec 08 14:49:01 2009 +0100
     2.2 +++ b/src/Tools/jEdit/plugin/Isabelle.props	Tue Dec 08 16:30:20 2009 +0100
     2.3 @@ -6,12 +6,11 @@
     2.4  plugin.isabelle.jedit.Plugin.name=Isabelle
     2.5  plugin.isabelle.jedit.Plugin.author=Johannes Hlzl, Fabian Immler, Makarius Wenzel
     2.6  plugin.isabelle.jedit.Plugin.version=0.0.1
     2.7 -plugin.isabelle.jedit.Plugin.description=Isabelle/Isar live document editing
     2.8 +plugin.isabelle.jedit.Plugin.description=Isabelle/Isar asynchronous proof processing
     2.9  
    2.10  #system parameters
    2.11  plugin.isabelle.jedit.Plugin.activate=defer
    2.12  plugin.isabelle.jedit.Plugin.usePluginHome=false
    2.13 -plugin.isabelle.jedit.Plugin.jars=
    2.14  
    2.15  #dependencies
    2.16  plugin.isabelle.jedit.Plugin.depend.0=jdk 1.6
    2.17 @@ -23,23 +22,23 @@
    2.18  #options
    2.19  plugin.isabelle.jedit.Plugin.option-pane=isabelle
    2.20  options.isabelle.label=Isabelle
    2.21 -options.isabelle.code=new isabelle.jedit.OptionPane();
    2.22 +options.isabelle.code=new isabelle.jedit.Isabelle_Options();
    2.23  options.isabelle.logic.title=Logic
    2.24  options.isabelle.font-size.title=Font Size
    2.25  options.isabelle.font-size=14
    2.26  
    2.27  #menu actions
    2.28  plugin.isabelle.jedit.Plugin.menu.label=Isabelle
    2.29 -plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-state isabelle.show-output isabelle.show-browser
    2.30 +plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-results isabelle.show-raw-output isabelle.show-history
    2.31  isabelle.activate.label=Activate current buffer
    2.32 -isabelle.show-state.label=Show State
    2.33 -isabelle.show-output.label=Show Output
    2.34 -isabelle.show-browser.label=Show Version-Browser
    2.35 +isabelle.show-results.label=Show Results
    2.36 +isabelle.show-raw-output.label=Show Raw Output
    2.37 +isabelle.show-history.label=Show History
    2.38  
    2.39  #dockables
    2.40 -isabelle-output.title=Isabelle Output
    2.41 -isabelle-state.title=Isabelle State
    2.42 -isabelle-browser.title=Isabelle Browse-Version
    2.43 +isabelle-results.title=Results
    2.44 +isabelle-raw-output.title=Raw Output
    2.45 +isabelle-history.title=History
    2.46  
    2.47  #SideKick
    2.48  sidekick.parser.isabelle.label=Isabelle
     3.1 --- a/src/Tools/jEdit/plugin/actions.xml	Tue Dec 08 14:49:01 2009 +0100
     3.2 +++ b/src/Tools/jEdit/plugin/actions.xml	Tue Dec 08 16:30:20 2009 +0100
     3.3 @@ -1,19 +1,7 @@
     3.4 +<?xml version="1.0"?>
     3.5 +<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
     3.6 +
     3.7  <ACTIONS>
     3.8 -	<ACTION NAME="isabelle.show-output">
     3.9 -		<CODE>
    3.10 -			wm.addDockableWindow("isabelle-output");
    3.11 -		</CODE>
    3.12 -	</ACTION>
    3.13 -	<ACTION NAME="isabelle.show-state">
    3.14 -		<CODE>
    3.15 -			wm.addDockableWindow("isabelle-state");
    3.16 -		</CODE>
    3.17 -	</ACTION>
    3.18 -  <ACTION NAME="isabelle.show-browser">
    3.19 -		<CODE>
    3.20 -			wm.addDockableWindow("isabelle-browser");
    3.21 -		</CODE>
    3.22 -	</ACTION>
    3.23    <ACTION NAME="isabelle.activate">
    3.24  		<CODE>
    3.25  			isabelle.jedit.Isabelle.plugin().switch_active(view);
    3.26 @@ -22,4 +10,19 @@
    3.27  			return isabelle.jedit.Isabelle.plugin().is_active(view.getBuffer());
    3.28  		</IS_SELECTED>
    3.29  	</ACTION>
    3.30 +	<ACTION NAME="isabelle.show-results">
    3.31 +		<CODE>
    3.32 +			wm.addDockableWindow("isabelle-results");
    3.33 +		</CODE>
    3.34 +	</ACTION>
    3.35 +	<ACTION NAME="isabelle.show-raw-output">
    3.36 +		<CODE>
    3.37 +			wm.addDockableWindow("isabelle-raw-output");
    3.38 +		</CODE>
    3.39 +	</ACTION>
    3.40 +  <ACTION NAME="isabelle.show-history">
    3.41 +		<CODE>
    3.42 +			wm.addDockableWindow("isabelle-history");
    3.43 +		</CODE>
    3.44 +	</ACTION>
    3.45  </ACTIONS>
    3.46 \ No newline at end of file
     4.1 --- a/src/Tools/jEdit/plugin/dockables.xml	Tue Dec 08 14:49:01 2009 +0100
     4.2 +++ b/src/Tools/jEdit/plugin/dockables.xml	Tue Dec 08 16:30:20 2009 +0100
     4.3 @@ -1,15 +1,14 @@
     4.4  <?xml version="1.0"?>
     4.5 -
     4.6  <!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
     4.7  
     4.8  <DOCKABLES>
     4.9 -	<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
    4.10 -		new isabelle.jedit.OutputDockable(view, position);
    4.11 +	<DOCKABLE NAME="isabelle-results" MOVABLE="TRUE">
    4.12 +		new isabelle.jedit.Results_Dockable(view, position).peer();
    4.13  	</DOCKABLE>
    4.14 -	<DOCKABLE NAME="isabelle-state" MOVABLE="TRUE">
    4.15 -		new isabelle.jedit.StateViewDockable(view, position);
    4.16 +	<DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
    4.17 +		new isabelle.jedit.Raw_Output_Dockable(view, position);
    4.18  	</DOCKABLE>
    4.19 -	<DOCKABLE NAME="isabelle-browser" MOVABLE="TRUE">
    4.20 -		new isabelle.jedit.BrowseVersionDockable(view, position).peer();
    4.21 +	<DOCKABLE NAME="isabelle-history" MOVABLE="TRUE">
    4.22 +		new isabelle.jedit.History_Dockable(view, position).peer();
    4.23  	</DOCKABLE>
    4.24  </DOCKABLES>
    4.25 \ No newline at end of file
     5.1 --- a/src/Tools/jEdit/plugin/services.xml	Tue Dec 08 14:49:01 2009 +0100
     5.2 +++ b/src/Tools/jEdit/plugin/services.xml	Tue Dec 08 16:30:20 2009 +0100
     5.3 @@ -1,13 +1,14 @@
     5.4  <?xml version="1.0"?>
     5.5  <!DOCTYPE SERVICES SYSTEM "services.dtd">
     5.6 +
     5.7  <SERVICES>
     5.8  	<SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
     5.9  		new isabelle.jedit.Isabelle_Encoding();
    5.10  	</SERVICE>
    5.11  	<SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
    5.12 -		new isabelle.jedit.IsabelleSideKickParser();
    5.13 +		new isabelle.jedit.Isabelle_Sidekick();
    5.14  	</SERVICE>
    5.15    <SERVICE NAME="isabelle" CLASS="gatchan.jedit.hyperlinks.HyperlinkSource">
    5.16 -    new isabelle.jedit.IsabelleHyperlinkSource();
    5.17 +    new isabelle.jedit.Isabelle_Hyperlinks();
    5.18    </SERVICE>
    5.19  </SERVICES>
     6.1 --- a/src/Tools/jEdit/src/jedit/browse_version_dockable.scala	Tue Dec 08 14:49:01 2009 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,43 +0,0 @@
     6.4 -/*
     6.5 - * Dockable window for navigating through the document-versions
     6.6 - *
     6.7 - * @author Fabian Immler, TU Munich
     6.8 - */
     6.9 -
    6.10 -package isabelle.jedit
    6.11 -
    6.12 -import isabelle.proofdocument.Change
    6.13 -
    6.14 -import java.awt.Dimension
    6.15 -import scala.swing.{ListView, FlowPanel}
    6.16 -import scala.swing.event.ListSelectionChanged
    6.17 -
    6.18 -import org.gjt.sp.jedit.View
    6.19 -import org.gjt.sp.jedit.gui.DockableWindowManager
    6.20 -
    6.21 -
    6.22 -class BrowseVersionDockable(view: View, position: String) extends FlowPanel
    6.23 -{
    6.24 -  if (position == DockableWindowManager.FLOATING)
    6.25 -    preferredSize = new Dimension(500, 250)
    6.26 -
    6.27 -  def prover_setup(): Option[ProverSetup] = Isabelle.prover_setup(view.getBuffer)
    6.28 -  def get_versions() =
    6.29 -    prover_setup() match {
    6.30 -      case None => Nil
    6.31 -      case Some(setup) => setup.theory_view.changes
    6.32 -    }
    6.33 -
    6.34 -  val list = new ListView[Change]
    6.35 -  list.fixedCellWidth = 500
    6.36 -  list.listData = get_versions()
    6.37 -  contents += list
    6.38 -
    6.39 -  listenTo(list.selection)
    6.40 -  reactions += {
    6.41 -    case ListSelectionChanged(source, range, false) =>
    6.42 -        prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
    6.43 -    }
    6.44 -
    6.45 -  prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
    6.46 -}
     7.1 --- a/src/Tools/jEdit/src/jedit/document_overview.scala	Tue Dec 08 14:49:01 2009 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit/document_overview.scala	Tue Dec 08 16:30:20 2009 +0100
     7.3 @@ -6,8 +6,8 @@
     7.4  
     7.5  package isabelle.jedit
     7.6  
     7.7 -import isabelle.prover.{Prover, Command}
     7.8 -import isabelle.proofdocument.ProofDocument
     7.9 +
    7.10 +import isabelle.proofdocument.{Command, Proof_Document, Prover, Theory_View}
    7.11  
    7.12  import javax.swing.{JPanel, ToolTipManager}
    7.13  import java.awt.event.{MouseAdapter, MouseEvent}
    7.14 @@ -21,7 +21,7 @@
    7.15  class Document_Overview(
    7.16      prover: Prover,
    7.17      text_area: JEditTextArea,
    7.18 -    to_current: (ProofDocument, Int) => Int)
    7.19 +    to_current: (Proof_Document, Int) => Int)
    7.20    extends JPanel(new BorderLayout)
    7.21  {
    7.22    private val WIDTH = 10
    7.23 @@ -67,7 +67,7 @@
    7.24        val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1
    7.25        val y = line_to_y(line1)
    7.26        val height = HEIGHT * (line2 - line1)
    7.27 -      gfx.setColor(TheoryView.choose_color(command, doc))
    7.28 +      gfx.setColor(Theory_View.choose_color(command, doc))
    7.29        gfx.fillRect(0, y, getWidth - 1, height)
    7.30      }
    7.31    }
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/jEdit/src/jedit/history_dockable.scala	Tue Dec 08 16:30:20 2009 +0100
     8.3 @@ -0,0 +1,44 @@
     8.4 +/*
     8.5 + * Dockable window for navigating through the document history
     8.6 + *
     8.7 + * @author Fabian Immler, TU Munich
     8.8 + */
     8.9 +
    8.10 +package isabelle.jedit
    8.11 +
    8.12 +
    8.13 +import isabelle.proofdocument.Change
    8.14 +
    8.15 +import java.awt.Dimension
    8.16 +import scala.swing.{ListView, FlowPanel}
    8.17 +import scala.swing.event.ListSelectionChanged
    8.18 +
    8.19 +import org.gjt.sp.jedit.View
    8.20 +import org.gjt.sp.jedit.gui.DockableWindowManager
    8.21 +
    8.22 +
    8.23 +class History_Dockable(view: View, position: String) extends FlowPanel
    8.24 +{
    8.25 +  if (position == DockableWindowManager.FLOATING)
    8.26 +    preferredSize = new Dimension(500, 250)
    8.27 +
    8.28 +  def prover_setup(): Option[Prover_Setup] = Isabelle.prover_setup(view.getBuffer)
    8.29 +  def get_versions() =
    8.30 +    prover_setup() match {
    8.31 +      case None => Nil
    8.32 +      case Some(setup) => setup.theory_view.changes
    8.33 +    }
    8.34 +
    8.35 +  val list = new ListView[Change]
    8.36 +  list.fixedCellWidth = 500
    8.37 +  list.listData = get_versions()
    8.38 +  contents += list
    8.39 +
    8.40 +  listenTo(list.selection)
    8.41 +  reactions += {
    8.42 +    case ListSelectionChanged(source, range, false) =>
    8.43 +      prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
    8.44 +  }
    8.45 +
    8.46 +  prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
    8.47 +}
     9.1 --- a/src/Tools/jEdit/src/jedit/isabelle_encoding.scala	Tue Dec 08 14:49:01 2009 +0100
     9.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala	Tue Dec 08 16:30:20 2009 +0100
     9.3 @@ -6,6 +6,7 @@
     9.4  
     9.5  package isabelle.jedit
     9.6  
     9.7 +
     9.8  import org.gjt.sp.jedit.io.Encoding
     9.9  import org.gjt.sp.jedit.buffer.JEditBuffer
    9.10  
    10.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Dec 08 14:49:01 2009 +0100
    10.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Dec 08 16:30:20 2009 +0100
    10.3 @@ -6,6 +6,7 @@
    10.4  
    10.5  package isabelle.jedit
    10.6  
    10.7 +
    10.8  import java.io.File
    10.9  
   10.10  import gatchan.jedit.hyperlinks.Hyperlink
   10.11 @@ -17,10 +18,10 @@
   10.12  import org.gjt.sp.jedit.Buffer
   10.13  import org.gjt.sp.jedit.TextUtilities
   10.14  
   10.15 -import isabelle.prover.Command
   10.16 +import isabelle.proofdocument.Command
   10.17  
   10.18  
   10.19 -class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
   10.20 +private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
   10.21    extends AbstractHyperlink(start, end, line, "")
   10.22  {
   10.23    override def click(view: View) {
   10.24 @@ -28,21 +29,22 @@
   10.25    }
   10.26  }
   10.27  
   10.28 -class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
   10.29 +class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
   10.30    extends AbstractHyperlink(start, end, line, "")
   10.31  {
   10.32    override def click(view: View) = {
   10.33      Isabelle.system.source_file(ref_file) match {
   10.34 -      case None => System.err.println("Could not find source file " + ref_file)
   10.35 +      case None => System.err.println("Could not find source file " + ref_file)  // FIXME ??
   10.36        case Some(file) =>
   10.37          jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
   10.38      }
   10.39    }
   10.40  }
   10.41  
   10.42 -class IsabelleHyperlinkSource extends HyperlinkSource
   10.43 +class Isabelle_Hyperlinks extends HyperlinkSource
   10.44  {
   10.45 -	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
   10.46 +	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
   10.47 +	{
   10.48      val prover = Isabelle.prover_setup(buffer).map(_.prover)
   10.49      val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
   10.50      if (prover.isEmpty || theory_view_opt.isEmpty) null
   10.51 @@ -61,11 +63,11 @@
   10.52                val end = theory_view.to_current(document, command_start + ref.stop)
   10.53                ref.info match {
   10.54                  case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
   10.55 -                  new ExternalHyperlink(begin, end, line, ref_file, ref_line)
   10.56 +                  new External_Hyperlink(begin, end, line, ref_file, ref_line)
   10.57                  case Command.RefInfo(_, _, Some(id), Some(offset)) =>
   10.58                    prover.get.command(id) match {
   10.59                      case Some(ref_cmd) =>
   10.60 -                      new InternalHyperlink(begin, end, line,
   10.61 +                      new Internal_Hyperlink(begin, end, line,
   10.62                          theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
   10.63                      case None => null
   10.64                    }
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala	Tue Dec 08 16:30:20 2009 +0100
    11.3 @@ -0,0 +1,44 @@
    11.4 +/*
    11.5 + * Editor pane for plugin options
    11.6 + *
    11.7 + * @author Johannes Hölzl, TU Munich
    11.8 + */
    11.9 +
   11.10 +package isabelle.jedit
   11.11 +
   11.12 +
   11.13 +import javax.swing.{JComboBox, JSpinner}
   11.14 +
   11.15 +import org.gjt.sp.jedit.AbstractOptionPane
   11.16 +
   11.17 +
   11.18 +class Isabelle_Options extends AbstractOptionPane("isabelle")
   11.19 +{
   11.20 +  private val logic_name = new JComboBox()
   11.21 +  private val font_size = new JSpinner()
   11.22 +
   11.23 +  override def _init()
   11.24 +  {
   11.25 +    addComponent(Isabelle.Property("logic.title"), {
   11.26 +      for (name <- Isabelle.system.find_logics()) {
   11.27 +        logic_name.addItem(name)
   11.28 +        if (name == Isabelle.Property("logic"))
   11.29 +          logic_name.setSelectedItem(name)
   11.30 +      }
   11.31 +      logic_name
   11.32 +    })
   11.33 +    addComponent(Isabelle.Property("font-size.title"), {
   11.34 +      font_size.setValue(Isabelle.Int_Property("font-size"))
   11.35 +      font_size
   11.36 +    })
   11.37 +  }
   11.38 +
   11.39 +  override def _save()
   11.40 +  {
   11.41 +    val logic = logic_name.getSelectedItem.asInstanceOf[String]
   11.42 +    Isabelle.Property("logic") = logic
   11.43 +
   11.44 +    val size = font_size.getValue().asInstanceOf[Int]
   11.45 +    Isabelle.Int_Property("font-size") = size
   11.46 +  }
   11.47 +}
    12.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Dec 08 14:49:01 2009 +0100
    12.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Dec 08 16:30:20 2009 +0100
    12.3 @@ -7,6 +7,7 @@
    12.4  
    12.5  package isabelle.jedit
    12.6  
    12.7 +
    12.8  import scala.collection.Set
    12.9  import scala.collection.immutable.TreeSet
   12.10  
   12.11 @@ -18,11 +19,10 @@
   12.12  import errorlist.DefaultErrorSource
   12.13  import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
   12.14  
   12.15 -import isabelle.prover.{Command, Markup_Node}
   12.16 -import isabelle.proofdocument.ProofDocument
   12.17 +import isabelle.proofdocument.{Command, Markup_Node, Proof_Document}
   12.18  
   12.19  
   12.20 -class IsabelleSideKickParser extends SideKickParser("isabelle")
   12.21 +class Isabelle_Sidekick extends SideKickParser("isabelle")
   12.22  {
   12.23    /* parsing */
   12.24  
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Tue Dec 08 16:30:20 2009 +0100
    13.3 @@ -0,0 +1,153 @@
    13.4 +/*
    13.5 + * include isabelle's command- and keyword-declarations
    13.6 + * live in jEdits syntax-highlighting
    13.7 + *
    13.8 + * @author Fabian Immler, TU Munich
    13.9 + */
   13.10 +
   13.11 +package isabelle.jedit
   13.12 +
   13.13 +
   13.14 +import isabelle.proofdocument.Prover
   13.15 +import isabelle.Markup
   13.16 +
   13.17 +import org.gjt.sp.jedit.buffer.JEditBuffer
   13.18 +import org.gjt.sp.jedit.syntax.{Token => JToken,
   13.19 +  TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
   13.20 +
   13.21 +import java.awt.Color
   13.22 +import java.awt.Font
   13.23 +import javax.swing.text.Segment;
   13.24 +
   13.25 +
   13.26 +object Isabelle_Token_Marker
   13.27 +{
   13.28 +  /* line context */
   13.29 +
   13.30 +  private val rule_set = new ParserRuleSet("isabelle", "MAIN")
   13.31 +  private class LineContext(val line: Int, prev: LineContext)
   13.32 +    extends TokenMarker.LineContext(rule_set, prev)
   13.33 +
   13.34 +
   13.35 +  /* mapping to jEdit token types */
   13.36 +  // TODO: as properties or CSS style sheet
   13.37 +
   13.38 +  private val choose_byte: Map[String, Byte] =
   13.39 +  {
   13.40 +    import JToken._
   13.41 +    Map[String, Byte](
   13.42 +      // logical entities
   13.43 +      Markup.TCLASS -> LABEL,
   13.44 +      Markup.TYCON -> LABEL,
   13.45 +      Markup.FIXED_DECL -> LABEL,
   13.46 +      Markup.FIXED -> LABEL,
   13.47 +      Markup.CONST_DECL -> LABEL,
   13.48 +      Markup.CONST -> LABEL,
   13.49 +      Markup.FACT_DECL -> LABEL,
   13.50 +      Markup.FACT -> LABEL,
   13.51 +      Markup.DYNAMIC_FACT -> LABEL,
   13.52 +      Markup.LOCAL_FACT_DECL -> LABEL,
   13.53 +      Markup.LOCAL_FACT -> LABEL,
   13.54 +      // inner syntax
   13.55 +      Markup.TFREE -> LITERAL2,
   13.56 +      Markup.FREE -> LITERAL2,
   13.57 +      Markup.TVAR -> LITERAL3,
   13.58 +      Markup.SKOLEM -> LITERAL3,
   13.59 +      Markup.BOUND -> LITERAL3,
   13.60 +      Markup.VAR -> LITERAL3,
   13.61 +      Markup.NUM -> DIGIT,
   13.62 +      Markup.FLOAT -> DIGIT,
   13.63 +      Markup.XNUM -> DIGIT,
   13.64 +      Markup.XSTR -> LITERAL4,
   13.65 +      Markup.LITERAL -> LITERAL4,
   13.66 +      Markup.INNER_COMMENT -> COMMENT1,
   13.67 +      Markup.SORT -> FUNCTION,
   13.68 +      Markup.TYP -> FUNCTION,
   13.69 +      Markup.TERM -> FUNCTION,
   13.70 +      Markup.PROP -> FUNCTION,
   13.71 +      Markup.ATTRIBUTE -> FUNCTION,
   13.72 +      Markup.METHOD -> FUNCTION,
   13.73 +      // ML syntax
   13.74 +      Markup.ML_KEYWORD -> KEYWORD2,
   13.75 +      Markup.ML_IDENT -> NULL,
   13.76 +      Markup.ML_TVAR -> LITERAL3,
   13.77 +      Markup.ML_NUMERAL -> DIGIT,
   13.78 +      Markup.ML_CHAR -> LITERAL1,
   13.79 +      Markup.ML_STRING -> LITERAL1,
   13.80 +      Markup.ML_COMMENT -> COMMENT1,
   13.81 +      Markup.ML_MALFORMED -> INVALID,
   13.82 +      // embedded source text
   13.83 +      Markup.ML_SOURCE -> COMMENT4,
   13.84 +      Markup.DOC_SOURCE -> COMMENT4,
   13.85 +      Markup.ANTIQ -> COMMENT4,
   13.86 +      Markup.ML_ANTIQ -> COMMENT4,
   13.87 +      Markup.DOC_ANTIQ -> COMMENT4,
   13.88 +      // outer syntax
   13.89 +      Markup.IDENT -> NULL,
   13.90 +      Markup.COMMAND -> OPERATOR,
   13.91 +      Markup.KEYWORD -> KEYWORD4,
   13.92 +      Markup.VERBATIM -> COMMENT3,
   13.93 +      Markup.COMMENT -> COMMENT1,
   13.94 +      Markup.CONTROL -> COMMENT3,
   13.95 +      Markup.MALFORMED -> INVALID,
   13.96 +      Markup.STRING -> LITERAL3,
   13.97 +      Markup.ALTSTRING -> LITERAL1
   13.98 +    ).withDefaultValue(NULL)
   13.99 +  }
  13.100 +
  13.101 +  def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
  13.102 +    styles(choose_byte(kind)).getForegroundColor
  13.103 +}
  13.104 +
  13.105 +
  13.106 +class Isabelle_Token_Marker(buffer: JEditBuffer, prover: Prover) extends TokenMarker
  13.107 +{
  13.108 +  override def markTokens(prev: TokenMarker.LineContext,
  13.109 +      handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
  13.110 +  {
  13.111 +    val previous = prev.asInstanceOf[Isabelle_Token_Marker.LineContext]
  13.112 +    val line = if (prev == null) 0 else previous.line + 1
  13.113 +    val context = new Isabelle_Token_Marker.LineContext(line, previous)
  13.114 +    val start = buffer.getLineStartOffset(line)
  13.115 +    val stop = start + line_segment.count
  13.116 +
  13.117 +    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
  13.118 +    val document = theory_view.current_document()
  13.119 +    def to: Int => Int = theory_view.to_current(document, _)
  13.120 +    def from: Int => Int = theory_view.from_current(document, _)
  13.121 +
  13.122 +    var next_x = start
  13.123 +    var cmd = document.command_at(from(start))
  13.124 +    while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
  13.125 +      val command = cmd.get
  13.126 +      for {
  13.127 +        markup <- command.highlight(document).flatten
  13.128 +        command_start = command.start(document)
  13.129 +        abs_start = to(command_start + markup.start)
  13.130 +        abs_stop = to(command_start + markup.stop)
  13.131 +        if (abs_stop > start)
  13.132 +        if (abs_start < stop)
  13.133 +        byte = Isabelle_Token_Marker.choose_byte(markup.info.toString)
  13.134 +        token_start = (abs_start - start) max 0
  13.135 +        token_length =
  13.136 +          (abs_stop - abs_start) -
  13.137 +          ((start - abs_start) max 0) -
  13.138 +          ((abs_stop - stop) max 0)
  13.139 +      } {
  13.140 +        if (start + token_start > next_x)
  13.141 +          handler.handleToken(line_segment, 1,
  13.142 +            next_x - start, start + token_start - next_x, context)
  13.143 +        handler.handleToken(line_segment, byte,
  13.144 +          token_start, token_length, context)
  13.145 +        next_x = start + token_start + token_length
  13.146 +      }
  13.147 +      cmd = document.commands.next(command)
  13.148 +    }
  13.149 +    if (next_x < stop)
  13.150 +      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
  13.151 +
  13.152 +    handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
  13.153 +    handler.setLineContext(context)
  13.154 +    return context
  13.155 +  }
  13.156 +}
    14.1 --- a/src/Tools/jEdit/src/jedit/option_pane.scala	Tue Dec 08 14:49:01 2009 +0100
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,43 +0,0 @@
    14.4 -/*
    14.5 - * Editor pane for plugin options
    14.6 - *
    14.7 - * @author Johannes Hölzl, TU Munich
    14.8 - */
    14.9 -
   14.10 -package isabelle.jedit
   14.11 -
   14.12 -import javax.swing.{JComboBox, JSpinner}
   14.13 -
   14.14 -import org.gjt.sp.jedit.AbstractOptionPane
   14.15 -
   14.16 -
   14.17 -class OptionPane extends AbstractOptionPane("isabelle")
   14.18 -{
   14.19 -  private val logic_name = new JComboBox()
   14.20 -  private val font_size = new JSpinner()
   14.21 -
   14.22 -  override def _init()
   14.23 -  {
   14.24 -    addComponent(Isabelle.Property("logic.title"), {
   14.25 -      for (name <- Isabelle.system.find_logics()) {
   14.26 -        logic_name.addItem(name)
   14.27 -        if (name == Isabelle.Property("logic"))
   14.28 -          logic_name.setSelectedItem(name)
   14.29 -      }
   14.30 -      logic_name
   14.31 -    })
   14.32 -    addComponent(Isabelle.Property("font-size.title"), {
   14.33 -      font_size.setValue(Isabelle.Int_Property("font-size"))
   14.34 -      font_size
   14.35 -    })
   14.36 -  }
   14.37 -
   14.38 -  override def _save()
   14.39 -  {
   14.40 -    val logic = logic_name.getSelectedItem.asInstanceOf[String]
   14.41 -    Isabelle.Property("logic") = logic
   14.42 -
   14.43 -    val size = font_size.getValue().asInstanceOf[Int]
   14.44 -    Isabelle.Int_Property("font-size") = size
   14.45 -  }
   14.46 -}
    15.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 14:49:01 2009 +0100
    15.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 16:30:20 2009 +0100
    15.3 @@ -3,6 +3,7 @@
    15.4   *
    15.5   * @author Johannes Hölzl, TU Munich
    15.6   * @author Fabian Immler, TU Munich
    15.7 + * @author Makarius
    15.8   */
    15.9  
   15.10  package isabelle.jedit
   15.11 @@ -14,8 +15,7 @@
   15.12  
   15.13  import scala.collection.mutable
   15.14  
   15.15 -import isabelle.prover.{Prover, Command}
   15.16 -import isabelle.proofdocument.ProofDocument
   15.17 +import isabelle.proofdocument.{Command, Proof_Document, Prover}
   15.18  import isabelle.Isabelle_System
   15.19  
   15.20  import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
   15.21 @@ -98,12 +98,12 @@
   15.22  
   15.23    /* mapping buffer <-> prover */
   15.24  
   15.25 -  private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
   15.26 +  private val mapping = new mutable.HashMap[JEditBuffer, Prover_Setup]
   15.27  
   15.28    private def install(view: View)
   15.29    {
   15.30      val buffer = view.getBuffer
   15.31 -    val prover_setup = new ProverSetup(buffer)
   15.32 +    val prover_setup = new Prover_Setup(buffer)
   15.33      mapping.update(buffer, prover_setup)
   15.34      prover_setup.activate(view)
   15.35    }
   15.36 @@ -115,7 +115,7 @@
   15.37      if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
   15.38      else install(view)
   15.39  
   15.40 -  def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
   15.41 +  def prover_setup(buffer: JEditBuffer): Option[Prover_Setup] = mapping.get(buffer)
   15.42    def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
   15.43  
   15.44  
    16.1 --- a/src/Tools/jEdit/src/jedit/prover_setup.scala	Tue Dec 08 14:49:01 2009 +0100
    16.2 +++ b/src/Tools/jEdit/src/jedit/prover_setup.scala	Tue Dec 08 16:30:20 2009 +0100
    16.3 @@ -9,18 +9,18 @@
    16.4  
    16.5  import org.gjt.sp.jedit.{Buffer, View}
    16.6  
    16.7 -import isabelle.prover.Prover
    16.8 +import isabelle.proofdocument.{Prover, Theory_View}
    16.9  
   16.10  
   16.11 -class ProverSetup(buffer: Buffer)
   16.12 +class Prover_Setup(buffer: Buffer)
   16.13  {
   16.14    var prover: Prover = null
   16.15 -  var theory_view: TheoryView = null
   16.16 +  var theory_view: Theory_View = null
   16.17  
   16.18    def activate(view: View)
   16.19    {
   16.20 -    // TheoryView starts prover
   16.21 -    theory_view = new TheoryView(view.getTextArea)
   16.22 +    // Theory_View starts prover
   16.23 +    theory_view = new Theory_View(view.getTextArea)
   16.24      prover = theory_view.prover
   16.25  
   16.26      theory_view.activate()
    17.1 --- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Tue Dec 08 14:49:01 2009 +0100
    17.2 +++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Tue Dec 08 16:30:20 2009 +0100
    17.3 @@ -15,8 +15,8 @@
    17.4  import org.gjt.sp.jedit.gui.DockableWindowManager
    17.5  
    17.6  
    17.7 -class OutputDockable(view : View, position : String) extends JPanel {
    17.8 -
    17.9 +class Raw_Output_Dockable(view: View, position: String) extends JPanel
   17.10 +{
   17.11    if (position == DockableWindowManager.FLOATING)
   17.12      setPreferredSize(new Dimension(500, 250))
   17.13  
    18.1 --- a/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 14:49:01 2009 +0100
    18.2 +++ b/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 16:30:20 2009 +0100
    18.3 @@ -7,13 +7,14 @@
    18.4  
    18.5  package isabelle.jedit
    18.6  
    18.7 +
    18.8  import isabelle.XML
    18.9  
   18.10 +import scala.swing.{BorderPanel, Component}
   18.11 +
   18.12  import java.io.StringReader
   18.13  import java.awt.{BorderLayout, Dimension}
   18.14 -
   18.15  import javax.swing.{JButton, JPanel, JScrollPane}
   18.16 -
   18.17  import java.util.logging.{Logger, Level}
   18.18  
   18.19  import org.lobobrowser.html.parser._
   18.20 @@ -31,12 +32,12 @@
   18.21  import scala.io.Source
   18.22  
   18.23  
   18.24 -class StateViewDockable(view : View, position : String) extends JPanel {
   18.25 -
   18.26 +class Results_Dockable(view : View, position : String) extends BorderPanel
   18.27 +{
   18.28    // outer panel
   18.29 +
   18.30    if (position == DockableWindowManager.FLOATING)
   18.31 -    setPreferredSize(new Dimension(500, 250))
   18.32 -  setLayout(new BorderLayout)
   18.33 +    preferredSize = new Dimension(500, 250)
   18.34  
   18.35  
   18.36    // global logging
   18.37 @@ -87,7 +88,8 @@
   18.38    doc.appendChild(empty_body)
   18.39  
   18.40    panel.setDocument(doc, rcontext)
   18.41 -  add(panel, BorderLayout.CENTER)
   18.42 +
   18.43 +  add(Component.wrap(panel), BorderPanel.Position.Center)
   18.44  
   18.45    
   18.46    // register for state-view
    19.1 --- a/src/Tools/jEdit/src/jedit/token_marker.scala	Tue Dec 08 14:49:01 2009 +0100
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,154 +0,0 @@
    19.4 -/*
    19.5 - * include isabelle's command- and keyword-declarations
    19.6 - * live in jEdits syntax-highlighting
    19.7 - *
    19.8 - * @author Fabian Immler, TU Munich
    19.9 - */
   19.10 -
   19.11 -package isabelle.jedit
   19.12 -
   19.13 -
   19.14 -import isabelle.prover.Prover
   19.15 -import isabelle.Markup
   19.16 -
   19.17 -import org.gjt.sp.jedit.buffer.JEditBuffer
   19.18 -import org.gjt.sp.jedit.syntax.{Token => JToken,
   19.19 -  TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
   19.20 -
   19.21 -import java.awt.Color
   19.22 -import java.awt.Font
   19.23 -import javax.swing.text.Segment;
   19.24 -
   19.25 -
   19.26 -object DynamicTokenMarker
   19.27 -{
   19.28 -  /* line context */
   19.29 -
   19.30 -  private val rule_set = new ParserRuleSet("isabelle", "MAIN")
   19.31 -  private class LineContext(val line: Int, prev: LineContext)
   19.32 -    extends TokenMarker.LineContext(rule_set, prev)
   19.33 -
   19.34 -
   19.35 -  /* mapping to jEdit token types */
   19.36 -  // TODO: as properties or CSS style sheet
   19.37 -
   19.38 -  private val choose_byte: Map[String, Byte] =
   19.39 -  {
   19.40 -    import JToken._
   19.41 -    Map[String, Byte](
   19.42 -      // logical entities
   19.43 -      Markup.TCLASS -> LABEL,
   19.44 -      Markup.TYCON -> LABEL,
   19.45 -      Markup.FIXED_DECL -> LABEL,
   19.46 -      Markup.FIXED -> LABEL,
   19.47 -      Markup.CONST_DECL -> LABEL,
   19.48 -      Markup.CONST -> LABEL,
   19.49 -      Markup.FACT_DECL -> LABEL,
   19.50 -      Markup.FACT -> LABEL,
   19.51 -      Markup.DYNAMIC_FACT -> LABEL,
   19.52 -      Markup.LOCAL_FACT_DECL -> LABEL,
   19.53 -      Markup.LOCAL_FACT -> LABEL,
   19.54 -      // inner syntax
   19.55 -      Markup.TFREE -> LITERAL2,
   19.56 -      Markup.FREE -> LITERAL2,
   19.57 -      Markup.TVAR -> LITERAL3,
   19.58 -      Markup.SKOLEM -> LITERAL3,
   19.59 -      Markup.BOUND -> LITERAL3,
   19.60 -      Markup.VAR -> LITERAL3,
   19.61 -      Markup.NUM -> DIGIT,
   19.62 -      Markup.FLOAT -> DIGIT,
   19.63 -      Markup.XNUM -> DIGIT,
   19.64 -      Markup.XSTR -> LITERAL4,
   19.65 -      Markup.LITERAL -> LITERAL4,
   19.66 -      Markup.INNER_COMMENT -> COMMENT1,
   19.67 -      Markup.SORT -> FUNCTION,
   19.68 -      Markup.TYP -> FUNCTION,
   19.69 -      Markup.TERM -> FUNCTION,
   19.70 -      Markup.PROP -> FUNCTION,
   19.71 -      Markup.ATTRIBUTE -> FUNCTION,
   19.72 -      Markup.METHOD -> FUNCTION,
   19.73 -      // ML syntax
   19.74 -      Markup.ML_KEYWORD -> KEYWORD2,
   19.75 -      Markup.ML_IDENT -> NULL,
   19.76 -      Markup.ML_TVAR -> LITERAL3,
   19.77 -      Markup.ML_NUMERAL -> DIGIT,
   19.78 -      Markup.ML_CHAR -> LITERAL1,
   19.79 -      Markup.ML_STRING -> LITERAL1,
   19.80 -      Markup.ML_COMMENT -> COMMENT1,
   19.81 -      Markup.ML_MALFORMED -> INVALID,
   19.82 -      // embedded source text
   19.83 -      Markup.ML_SOURCE -> COMMENT4,
   19.84 -      Markup.DOC_SOURCE -> COMMENT4,
   19.85 -      Markup.ANTIQ -> COMMENT4,
   19.86 -      Markup.ML_ANTIQ -> COMMENT4,
   19.87 -      Markup.DOC_ANTIQ -> COMMENT4,
   19.88 -      // outer syntax
   19.89 -      Markup.IDENT -> NULL,
   19.90 -      Markup.COMMAND -> OPERATOR,
   19.91 -      Markup.KEYWORD -> KEYWORD4,
   19.92 -      Markup.VERBATIM -> COMMENT3,
   19.93 -      Markup.COMMENT -> COMMENT1,
   19.94 -      Markup.CONTROL -> COMMENT3,
   19.95 -      Markup.MALFORMED -> INVALID,
   19.96 -      Markup.STRING -> LITERAL3,
   19.97 -      Markup.ALTSTRING -> LITERAL1
   19.98 -    ).withDefaultValue(NULL)
   19.99 -  }
  19.100 -
  19.101 -  def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
  19.102 -    styles(choose_byte(kind)).getForegroundColor
  19.103 -}
  19.104 -
  19.105 -
  19.106 -class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover)
  19.107 -  extends TokenMarker
  19.108 -{
  19.109 -  override def markTokens(prev: TokenMarker.LineContext,
  19.110 -      handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
  19.111 -  {
  19.112 -    val previous = prev.asInstanceOf[DynamicTokenMarker.LineContext]
  19.113 -    val line = if (prev == null) 0 else previous.line + 1
  19.114 -    val context = new DynamicTokenMarker.LineContext(line, previous)
  19.115 -    val start = buffer.getLineStartOffset(line)
  19.116 -    val stop = start + line_segment.count
  19.117 -
  19.118 -    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
  19.119 -    val document = theory_view.current_document()
  19.120 -    def to: Int => Int = theory_view.to_current(document, _)
  19.121 -    def from: Int => Int = theory_view.from_current(document, _)
  19.122 -
  19.123 -    var next_x = start
  19.124 -    var cmd = document.command_at(from(start))
  19.125 -    while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
  19.126 -      val command = cmd.get
  19.127 -      for {
  19.128 -        markup <- command.highlight(document).flatten
  19.129 -        command_start = command.start(document)
  19.130 -        abs_start = to(command_start + markup.start)
  19.131 -        abs_stop = to(command_start + markup.stop)
  19.132 -        if (abs_stop > start)
  19.133 -        if (abs_start < stop)
  19.134 -        byte = DynamicTokenMarker.choose_byte(markup.info.toString)
  19.135 -        token_start = (abs_start - start) max 0
  19.136 -        token_length =
  19.137 -          (abs_stop - abs_start) -
  19.138 -          ((start - abs_start) max 0) -
  19.139 -          ((abs_stop - stop) max 0)
  19.140 -      } {
  19.141 -        if (start + token_start > next_x)
  19.142 -          handler.handleToken(line_segment, 1,
  19.143 -            next_x - start, start + token_start - next_x, context)
  19.144 -        handler.handleToken(line_segment, byte,
  19.145 -          token_start, token_length, context)
  19.146 -        next_x = start + token_start + token_length
  19.147 -      }
  19.148 -      cmd = document.commands.next(command)
  19.149 -    }
  19.150 -    if (next_x < stop)
  19.151 -      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
  19.152 -
  19.153 -    handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
  19.154 -    handler.setLineContext(context)
  19.155 -    return context
  19.156 -  }
  19.157 -}
    20.1 --- a/src/Tools/jEdit/src/proofdocument/command.scala	Tue Dec 08 14:49:01 2009 +0100
    20.2 +++ b/src/Tools/jEdit/src/proofdocument/command.scala	Tue Dec 08 16:30:20 2009 +0100
    20.3 @@ -5,14 +5,13 @@
    20.4   * @author Fabian Immler, TU Munich
    20.5   */
    20.6  
    20.7 -package isabelle.prover
    20.8 +package isabelle.proofdocument
    20.9  
   20.10  
   20.11  import scala.actors.Actor, Actor._
   20.12  
   20.13  import scala.collection.mutable
   20.14  
   20.15 -import isabelle.proofdocument.{Token, ProofDocument}
   20.16  import isabelle.jedit.{Isabelle, Plugin}
   20.17  import isabelle.XML
   20.18  
   20.19 @@ -70,8 +69,8 @@
   20.20    def content(i: Int, j: Int): String = content.substring(i, j)
   20.21    val symbol_index = new Symbol.Index(content)
   20.22  
   20.23 -  def start(doc: ProofDocument) = doc.token_start(tokens.first)
   20.24 -  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
   20.25 +  def start(doc: Proof_Document) = doc.token_start(tokens.first)
   20.26 +  def stop(doc: Proof_Document) = doc.token_start(tokens.last) + tokens.last.length
   20.27  
   20.28    def contains(p: Token) = tokens.contains(p)
   20.29  
   20.30 @@ -93,15 +92,15 @@
   20.31    /* results, markup, ... */
   20.32  
   20.33    private val empty_cmd_state = new Command_State(this)
   20.34 -  private def cmd_state(doc: ProofDocument) =
   20.35 +  private def cmd_state(doc: Proof_Document) =
   20.36      doc.states.getOrElse(this, empty_cmd_state)
   20.37  
   20.38 -  def status(doc: ProofDocument) = cmd_state(doc).state.status
   20.39 -  def results(doc: ProofDocument) = cmd_state(doc).results
   20.40 -  def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
   20.41 -  def highlight(doc: ProofDocument) = cmd_state(doc).highlight
   20.42 -  def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
   20.43 -  def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
   20.44 +  def status(doc: Proof_Document) = cmd_state(doc).state.status
   20.45 +  def results(doc: Proof_Document) = cmd_state(doc).results
   20.46 +  def markup_root(doc: Proof_Document) = cmd_state(doc).markup_root
   20.47 +  def highlight(doc: Proof_Document) = cmd_state(doc).highlight
   20.48 +  def type_at(doc: Proof_Document, offset: Int) = cmd_state(doc).type_at(offset)
   20.49 +  def ref_at(doc: Proof_Document, offset: Int) = cmd_state(doc).ref_at(offset)
   20.50  }
   20.51  
   20.52  
    21.1 --- a/src/Tools/jEdit/src/proofdocument/markup_node.scala	Tue Dec 08 14:49:01 2009 +0100
    21.2 +++ b/src/Tools/jEdit/src/proofdocument/markup_node.scala	Tue Dec 08 16:30:20 2009 +0100
    21.3 @@ -2,14 +2,14 @@
    21.4   * Document markup nodes, with connection to Swing tree model
    21.5   *
    21.6   * @author Fabian Immler, TU Munich
    21.7 + * @author Makarius
    21.8   */
    21.9  
   21.10 -package isabelle.prover
   21.11 +package isabelle.proofdocument
   21.12  
   21.13  
   21.14  import javax.swing.tree.DefaultMutableTreeNode
   21.15  
   21.16 -import isabelle.proofdocument.ProofDocument
   21.17  
   21.18  
   21.19  class Markup_Node(val start: Int, val stop: Int, val info: Any)
    22.1 --- a/src/Tools/jEdit/src/proofdocument/proof_document.scala	Tue Dec 08 14:49:01 2009 +0100
    22.2 +++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala	Tue Dec 08 16:30:20 2009 +0100
    22.3 @@ -8,14 +8,13 @@
    22.4  
    22.5  package isabelle.proofdocument
    22.6  
    22.7 +
    22.8  import scala.actors.Actor, Actor._
    22.9  
   22.10  import java.util.regex.Pattern
   22.11  
   22.12 -import isabelle.prover.{Prover, Command, Command_State}
   22.13  
   22.14 -
   22.15 -object ProofDocument
   22.16 +object Proof_Document
   22.17  {
   22.18    // Be careful when changing this regex. Not only must it handle the
   22.19    // spurious end of a token but also:  
   22.20 @@ -34,14 +33,14 @@
   22.21        "[()\\[\\]{}:;]", Pattern.MULTILINE)
   22.22  
   22.23    val empty =
   22.24 -    new ProofDocument(isabelle.jedit.Isabelle.system.id(),
   22.25 +    new Proof_Document(isabelle.jedit.Isabelle.system.id(),
   22.26        Linear_Set(), Map(), Linear_Set(), Map(), _ => false)
   22.27  
   22.28    type StructureChange = List[(Option[Command], Option[Command])]
   22.29  
   22.30  }
   22.31  
   22.32 -class ProofDocument(
   22.33 +class Proof_Document(
   22.34    val id: String,
   22.35    val tokens: Linear_Set[Token],
   22.36    val token_start: Map[Token, Int],
   22.37 @@ -49,10 +48,10 @@
   22.38    var states: Map[Command, Command_State],   // FIXME immutable
   22.39    is_command_keyword: String => Boolean)
   22.40  {
   22.41 -  import ProofDocument.StructureChange
   22.42 +  import Proof_Document.StructureChange
   22.43  
   22.44 -  def set_command_keyword(f: String => Boolean): ProofDocument =
   22.45 -    new ProofDocument(id, tokens, token_start, commands, states, f)
   22.46 +  def set_command_keyword(f: String => Boolean): Proof_Document =
   22.47 +    new Proof_Document(id, tokens, token_start, commands, states, f)
   22.48  
   22.49    def content = Token.string_from_tokens(Nil ++ tokens, token_start)
   22.50  
   22.51 @@ -60,9 +59,9 @@
   22.52    
   22.53    /** token view **/
   22.54  
   22.55 -  def text_changed(change: Change): (ProofDocument, StructureChange) =
   22.56 +  def text_changed(change: Change): (Proof_Document, StructureChange) =
   22.57    {
   22.58 -    def edit_doc(doc_chgs: (ProofDocument, StructureChange), edit: Edit) = {
   22.59 +    def edit_doc(doc_chgs: (Proof_Document, StructureChange), edit: Edit) = {
   22.60        val (doc, chgs) = doc_chgs
   22.61        val (new_doc, chg) = doc.text_edit(edit, change.id)
   22.62        (new_doc, chgs ++ chg)
   22.63 @@ -70,7 +69,7 @@
   22.64      ((this, Nil: StructureChange) /: change.edits)(edit_doc)
   22.65    }
   22.66  
   22.67 -  def text_edit(e: Edit, id: String): (ProofDocument, StructureChange) =
   22.68 +  def text_edit(e: Edit, id: String): (Proof_Document, StructureChange) =
   22.69    {
   22.70      case class TextChange(start: Int, added: String, removed: String)
   22.71      val change = e match {
   22.72 @@ -116,7 +115,7 @@
   22.73  
   22.74      val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
   22.75      val matcher =
   22.76 -      ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
   22.77 +      Proof_Document.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
   22.78  
   22.79      while (matcher.find() && invalid_tokens != Nil) {
   22.80  			val kind =
   22.81 @@ -158,7 +157,7 @@
   22.82      after_change: Option[Token],
   22.83      new_tokens: List[Token],
   22.84      new_token_start: Map[Token, Int]):
   22.85 -  (ProofDocument, StructureChange) =
   22.86 +  (Proof_Document, StructureChange) =
   22.87    {
   22.88      val new_tokenset = Linear_Set[Token]() ++ new_tokens
   22.89      val cmd_before_change = before_change match {
   22.90 @@ -236,7 +235,7 @@
   22.91  
   22.92  
   22.93      val doc =
   22.94 -      new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
   22.95 +      new Proof_Document(new_id, new_tokenset, new_token_start, new_commandset,
   22.96          states -- removed_commands, is_command_keyword)
   22.97  
   22.98      val removes =
    23.1 --- a/src/Tools/jEdit/src/proofdocument/prover.scala	Tue Dec 08 14:49:01 2009 +0100
    23.2 +++ b/src/Tools/jEdit/src/proofdocument/prover.scala	Tue Dec 08 16:30:20 2009 +0100
    23.3 @@ -6,7 +6,7 @@
    23.4   * @author Makarius
    23.5   */
    23.6  
    23.7 -package isabelle.prover
    23.8 +package isabelle.proofdocument
    23.9  
   23.10  
   23.11  import scala.actors.Actor, Actor._
   23.12 @@ -14,7 +14,6 @@
   23.13  import javax.swing.JTextArea
   23.14  
   23.15  import isabelle.jedit.Isabelle
   23.16 -import isabelle.proofdocument.{ProofDocument, Change, Token}
   23.17  
   23.18  
   23.19  class Prover(system: Isabelle_System, logic: String)
   23.20 @@ -41,7 +40,7 @@
   23.21    /* outgoing messages */
   23.22  
   23.23    val command_change = new Event_Bus[Command]
   23.24 -  val document_change = new Event_Bus[ProofDocument]
   23.25 +  val document_change = new Event_Bus[Proof_Document]
   23.26  
   23.27  
   23.28    /* prover process */
   23.29 @@ -67,12 +66,12 @@
   23.30    @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
   23.31    @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
   23.32    val document_0 =
   23.33 -    ProofDocument.empty.
   23.34 +    Proof_Document.empty.
   23.35      set_command_keyword((s: String) => command_decls().contains(s))
   23.36    @volatile private var document_versions = List(document_0)
   23.37  
   23.38    def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
   23.39 -  def document(id: Isar_Document.Document_ID): Option[ProofDocument] =
   23.40 +  def document(id: Isar_Document.Document_ID): Option[Proof_Document] =
   23.41      document_versions.find(_.id == id)
   23.42  
   23.43  
    24.1 --- a/src/Tools/jEdit/src/proofdocument/state.scala	Tue Dec 08 14:49:01 2009 +0100
    24.2 +++ b/src/Tools/jEdit/src/proofdocument/state.scala	Tue Dec 08 16:30:20 2009 +0100
    24.3 @@ -5,7 +5,7 @@
    24.4   * @author Makarius
    24.5   */
    24.6  
    24.7 -package isabelle.prover
    24.8 +package isabelle.proofdocument
    24.9  
   24.10  
   24.11  class State(
    25.1 --- a/src/Tools/jEdit/src/proofdocument/theory_view.scala	Tue Dec 08 14:49:01 2009 +0100
    25.2 +++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala	Tue Dec 08 16:30:20 2009 +0100
    25.3 @@ -6,14 +6,12 @@
    25.4   * @author Makarius
    25.5   */
    25.6  
    25.7 -package isabelle.jedit
    25.8 +package isabelle.proofdocument
    25.9 +
   25.10  
   25.11  import scala.actors.Actor, Actor._
   25.12  import scala.collection.mutable
   25.13  
   25.14 -import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove}
   25.15 -import isabelle.prover.{Prover, Command}
   25.16 -
   25.17  import java.awt.{Color, Graphics2D}
   25.18  import javax.swing.event.{CaretListener, CaretEvent}
   25.19  
   25.20 @@ -21,10 +19,12 @@
   25.21  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
   25.22  import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
   25.23  
   25.24 +import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker, Raw_Output_Dockable}
   25.25  
   25.26 -object TheoryView
   25.27 +
   25.28 +object Theory_View
   25.29  {
   25.30 -  def choose_color(command: Command, doc: ProofDocument): Color =
   25.31 +  def choose_color(command: Command, doc: Proof_Document): Color =
   25.32    {
   25.33      command.status(doc) match {
   25.34        case Command.Status.UNPROCESSED => new Color(255, 228, 225)
   25.35 @@ -36,7 +36,7 @@
   25.36  }
   25.37  
   25.38  
   25.39 -class TheoryView(text_area: JEditTextArea)
   25.40 +class Theory_View(text_area: JEditTextArea)
   25.41  {
   25.42    private val buffer = text_area.getBuffer
   25.43  
   25.44 @@ -115,8 +115,8 @@
   25.45        screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   25.46      {
   25.47        val document = current_document()
   25.48 -      def from_current(pos: Int) = TheoryView.this.from_current(document, pos)
   25.49 -      def to_current(pos: Int) = TheoryView.this.to_current(document, pos)
   25.50 +      def from_current(pos: Int) = Theory_View.this.from_current(document, pos)
   25.51 +      def to_current(pos: Int) = Theory_View.this.to_current(document, pos)
   25.52        val saved_color = gfx.getColor
   25.53  
   25.54        val metrics = text_area.getPainter.getFontMetrics
   25.55 @@ -128,7 +128,7 @@
   25.56          val begin = start max to_current(e.start(document))
   25.57          val finish = (end - 1) min to_current(e.stop(document))
   25.58          encolor(gfx, y, metrics.getHeight, begin, finish,
   25.59 -          TheoryView.choose_color(e, document), true)
   25.60 +          Theory_View.choose_color(e, document), true)
   25.61          cmd = document.commands.next(e)
   25.62        }
   25.63  
   25.64 @@ -166,18 +166,19 @@
   25.65      }
   25.66    }
   25.67  
   25.68 -  def activate() {
   25.69 +  def activate()
   25.70 +  {
   25.71      text_area.addCaretListener(selected_state_controller)
   25.72      text_area.addLeftOfScrollBar(overview)
   25.73      text_area.getPainter.
   25.74        addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
   25.75 -    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
   25.76 +    buffer.setTokenMarker(new Isabelle_Token_Marker(buffer, prover))
   25.77      buffer.addBufferListener(buffer_listener)
   25.78  
   25.79      val dockable =
   25.80 -      text_area.getView.getDockableWindowManager.getDockable("isabelle-output")
   25.81 +      text_area.getView.getDockableWindowManager.getDockable("isabelle-raw-output")
   25.82      if (dockable != null) {
   25.83 -      val output_dockable = dockable.asInstanceOf[OutputDockable]
   25.84 +      val output_dockable = dockable.asInstanceOf[Raw_Output_Dockable]
   25.85        val output_text_view = prover.output_text_view
   25.86        output_dockable.set_text(output_text_view)
   25.87      }
   25.88 @@ -196,7 +197,7 @@
   25.89  
   25.90    /* history of changes */
   25.91  
   25.92 -  private def doc_or_pred(c: Change): ProofDocument =
   25.93 +  private def doc_or_pred(c: Change): Proof_Document =
   25.94      prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
   25.95  
   25.96    def current_document() = doc_or_pred(current_change)
   25.97 @@ -254,14 +255,14 @@
   25.98  
   25.99    /* transforming offsets */
  25.100  
  25.101 -  private def changes_from(doc: ProofDocument): List[Edit] =
  25.102 +  private def changes_from(doc: Proof_Document): List[Edit] =
  25.103      List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
  25.104        edits.toList
  25.105  
  25.106 -  def from_current(doc: ProofDocument, offset: Int): Int =
  25.107 +  def from_current(doc: Proof_Document, offset: Int): Int =
  25.108      (offset /: changes_from(doc).reverse) ((i, change) => change before i)
  25.109  
  25.110 -  def to_current(doc: ProofDocument, offset: Int): Int =
  25.111 +  def to_current(doc: Proof_Document, offset: Int): Int =
  25.112      (offset /: changes_from(doc)) ((i, change) => change after i)
  25.113  
  25.114  
    26.1 --- a/src/Tools/jEdit/src/proofdocument/token.scala	Tue Dec 08 14:49:01 2009 +0100
    26.2 +++ b/src/Tools/jEdit/src/proofdocument/token.scala	Tue Dec 08 16:30:20 2009 +0100
    26.3 @@ -8,9 +8,6 @@
    26.4  package isabelle.proofdocument
    26.5  
    26.6  
    26.7 -import isabelle.prover.Command
    26.8 -
    26.9 -
   26.10  object Token {
   26.11    object Kind extends Enumeration
   26.12    {