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 Hölzl, 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 {