# HG changeset patch
# User wenzelm
# Date 1348605366 -7200
# Node ID 66cbf8bb46933cb0c10fc4218a21c9bd8448655c
# Parent ea4308b7ef0ff0c54d5791f2ce768552cbfb2db7
basic integration of graphview into document model;
added Graph_Dockable;
updated Isabelle/jEdit authors and dependencies etc.;
diff -r ea4308b7ef0f -r 66cbf8bb4693 src/Pure/General/graph_display.ML
--- a/src/Pure/General/graph_display.ML Tue Sep 25 20:28:47 2012 +0200
+++ b/src/Pure/General/graph_display.ML Tue Sep 25 22:36:06 2012 +0200
@@ -13,6 +13,7 @@
val write_graph_browser: Path.T -> graph -> unit
val browserN: string
val graphviewN: string
+ val graphview_reportN: string
val display_graph: graph -> unit
end;
@@ -32,6 +33,7 @@
val browserN = "browser";
val graphviewN = "graphview";
+val graphview_reportN = "graphview_report";
fun write_graph_browser path (graph: graph) =
File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
@@ -54,19 +56,24 @@
(* display graph *)
fun display_graph graph =
- let
- val browser =
- (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
- SOME m => m = browserN
- | NONE => true);
- val (write, tool) =
- if browser then (write_graph_browser, "browser") else (write_graph_graphview, "graphview");
+ if print_mode_active graphview_reportN then
+ Output.report
+ (YXML.string_of (XML.Elem ((Isabelle_Markup.graphviewN, []), encode_graphview graph)))
+ else
+ let
+ val browser =
+ (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
+ SOME m => m = browserN
+ | NONE => true);
+ val (write, tool) =
+ if browser then (write_graph_browser, "browser")
+ else (write_graph_graphview, "graphview");
- val _ = writeln "Displaying graph ...";
- val path = Isabelle_System.create_tmp_path "graph" "";
- val _ = write path graph;
- val _ = Isabelle_System.isabelle_tool tool ("-c " ^ File.shell_path path ^ " &");
- in () end;
+ val _ = writeln "Displaying graph ...";
+ val path = Isabelle_System.create_tmp_path "graph" "";
+ val _ = write path graph;
+ val _ = Isabelle_System.isabelle_tool tool ("-c " ^ File.shell_path path ^ " &");
+ in () end;
end;
diff -r ea4308b7ef0f -r 66cbf8bb4693 src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML Tue Sep 25 20:28:47 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML Tue Sep 25 22:36:06 2012 +0200
@@ -100,6 +100,7 @@
val reportN: string val report: Markup.T
val no_reportN: string val no_report: Markup.T
val badN: string val bad: Markup.T
+ val graphviewN: string
val functionN: string
val assign_execs: Properties.T
val removed_versions: Properties.T
@@ -296,6 +297,8 @@
val (badN, bad) = markup_elem "bad";
+val graphviewN = "graphview";
+
(* protocol message functions *)
diff -r ea4308b7ef0f -r 66cbf8bb4693 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala Tue Sep 25 20:28:47 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala Tue Sep 25 22:36:06 2012 +0200
@@ -254,6 +254,8 @@
val BAD = "bad"
+ val GRAPHVIEW = "graphview"
+
/* protocol message functions */
diff -r ea4308b7ef0f -r 66cbf8bb4693 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML Tue Sep 25 20:28:47 2012 +0200
+++ b/src/Pure/System/isabelle_process.ML Tue Sep 25 22:36:06 2012 +0200
@@ -161,6 +161,10 @@
(* init *)
+val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
+val default_modes2 =
+ [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN, Graph_Display.graphview_reportN];
+
fun init rendezvous = ignore (Simple_Thread.fork false (fn () =>
let
val _ = OS.Process.sleep (seconds 0.5); (*yield to raw ML toplevel*)
@@ -174,9 +178,7 @@
val _ = Context.set_thread_data NONE;
val _ =
Unsynchronized.change print_mode
- (fn mode =>
- (mode @ [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN])
- |> fold (update op =) [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]);
+ (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
val channel = rendezvous ();
val _ = init_channels channel;
diff -r ea4308b7ef0f -r 66cbf8bb4693 src/Tools/Graphview/src/dockable.scala
--- a/src/Tools/Graphview/src/dockable.scala Tue Sep 25 20:28:47 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-/* Title: Tools/Graphview/src/dockable.scala
- Author: Markus Kaiser, TU Muenchen
-
-Graphview jEdit dockable.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-import isabelle.jedit._
-
-import scala.actors.Actor._
-import scala.swing.{FileChooser}
-
-import java.io.File
-import org.gjt.sp.jedit.View
-
-
-class Graphview_Dockable(view: View, position: String)
-extends Dockable(view, position)
-{
- //FIXME: How does the xml get here?
- val xml: XML.Tree =
- try {
- val chooser = new FileChooser()
- val path: File = chooser.showOpenDialog(null) match {
- case FileChooser.Result.Approve =>
- chooser.selectedFile
- case _ => new File("~/local_deps.graph")
- }
- YXML.parse_body(Symbol.decode(io.Source.fromFile(path).mkString)).head
- } catch {
- case ex: Exception => System.err.println(ex.getMessage); null
- }
-
-
- set_content(new Main_Panel(xml))
-
- /* main actor */
-
- private val main_actor = actor {
- loop {
- react {
- case result: Isabelle_Process.Output =>
- case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
- }
- }
- }
-
- override def init() { }
- override def exit() { }
-}
diff -r ea4308b7ef0f -r 66cbf8bb4693 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Sep 25 20:28:47 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Sep 25 22:36:06 2012 +0200
@@ -12,6 +12,7 @@
"src/document_model.scala"
"src/document_view.scala"
"src/html_panel.scala"
+ "src/graph_dockable.scala"
"src/hyperlink.scala"
"src/isabelle_encoding.scala"
"src/isabelle_logic.scala"
@@ -89,6 +90,7 @@
BUILD_ONLY=false
BUILD_JARS="jars"
+FRESH_OPTION=""
JEDIT_SESSION_DIRS=""
JEDIT_LOGIC="$ISABELLE_LOGIC"
JEDIT_PRINT_MODE=""
@@ -113,6 +115,7 @@
fi
;;
f)
+ FRESH_OPTION="-f"
BUILD_JARS="jars_fresh"
;;
j)
@@ -162,9 +165,13 @@
## dependencies
[ -e "$ISABELLE_HOME/Admin/build" ] && \
- { "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?; }
+ {
+ "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
+ "$ISABELLE_TOOL" graphview -b $FRESH_OPTION || exit $?
+ }
PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
+GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/ext/Graphview.jar"
pushd "$JEDIT_HOME" >/dev/null || failed
@@ -193,9 +200,12 @@
OUTDATED=true
else
if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
- declare -a DEPS=("$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
+ declare -a DEPS=(
+ "$JEDIT_JAR" "${JEDIT_JARS[@]}"
+ "$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
+ )
elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
- declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
+ declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
else
declare -a DEPS=()
fi
@@ -247,7 +257,8 @@
cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
(
- for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
+ for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR" \
+ "$SCALA_HOME/lib/scala-compiler.jar"
do
CLASSPATH="$CLASSPATH:$JAR"
done
diff -r ea4308b7ef0f -r 66cbf8bb4693 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props Tue Sep 25 20:28:47 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Tue Sep 25 22:36:06 2012 +0200
@@ -4,20 +4,20 @@
#identification
plugin.isabelle.jedit.Plugin.name=Isabelle
-plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Makarius Wenzel
-plugin.isabelle.jedit.Plugin.version=0.1.0
-plugin.isabelle.jedit.Plugin.description=Isabelle/Isar asynchronous proof document editing
+plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Markus Kaiser, Makarius Wenzel
+plugin.isabelle.jedit.Plugin.version=1.0.0
+plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE
#system parameters
plugin.isabelle.jedit.Plugin.activate=startup
plugin.isabelle.jedit.Plugin.usePluginHome=false
#dependencies
-plugin.isabelle.jedit.Plugin.depend.0=jdk 1.6
-plugin.isabelle.jedit.Plugin.depend.1=jedit 04.03.99.00
-plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 4.4.1
-plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 1.8
-plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 0.8
+plugin.isabelle.jedit.Plugin.depend.0=jdk 1.7
+plugin.isabelle.jedit.Plugin.depend.1=jedit 04.05.02.00
+plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 4.5
+plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 1.9
+plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.3
#options
plugin.isabelle.jedit.Plugin.option-group=isabelle-general isabelle-rendering
@@ -40,9 +40,10 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.output1-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel
+plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.graph-panel isabelle.output1-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel
isabelle.session-panel.label=Prover Session panel
isabelle.output-panel.label=Output panel
+isabelle.graph-panel.label=Graph panel
isabelle.output1-panel.label=Output1 panel
isabelle.raw-output-panel.label=Raw Output panel
isabelle.protocol-panel.label=Protocol panel
@@ -52,6 +53,7 @@
#dockables
isabelle-session.title=Prover Session
isabelle-output.title=Output
+isabelle-graph.title=Graph
isabelle-output1.title=Output1
isabelle-raw-output.title=Raw Output
isabelle-protocol.title=Protocol
diff -r ea4308b7ef0f -r 66cbf8bb4693 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml Tue Sep 25 20:28:47 2012 +0200
+++ b/src/Tools/jEdit/src/actions.xml Tue Sep 25 22:36:06 2012 +0200
@@ -27,6 +27,11 @@
wm.addDockableWindow("isabelle-output1");
+
+
+ wm.addDockableWindow("isabelle-graph");
+
+
wm.addDockableWindow("isabelle-raw-output");
diff -r ea4308b7ef0f -r 66cbf8bb4693 src/Tools/jEdit/src/dockables.xml
--- a/src/Tools/jEdit/src/dockables.xml Tue Sep 25 20:28:47 2012 +0200
+++ b/src/Tools/jEdit/src/dockables.xml Tue Sep 25 22:36:06 2012 +0200
@@ -14,6 +14,9 @@
new isabelle.jedit.Output_Dockable(view, position);
+
+ new isabelle.jedit.Graph_Dockable(view, position);
+
new isabelle.jedit.Output1_Dockable(view, position);
diff -r ea4308b7ef0f -r 66cbf8bb4693 src/Tools/jEdit/src/graph_dockable.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/graph_dockable.scala Tue Sep 25 22:36:06 2012 +0200
@@ -0,0 +1,131 @@
+/* Title: Tools/jEdit/src/graph_dockable.scala
+ Author: Markus Kaiser, TU Muenchen
+ Author: Makarius
+
+Dockable window for graphview.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.BorderLayout
+import javax.swing.JPanel
+
+import scala.actors.Actor._
+
+import org.gjt.sp.jedit.View
+
+
+class Graph_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+ Swing_Thread.require()
+
+
+ /* component state -- owned by Swing thread */
+
+ private val do_update = true // FIXME
+
+ private var current_snapshot = Document.State.init.snapshot()
+ private var current_state = Command.empty.init_state
+ private var current_graph: XML.Body = Nil
+
+
+ /* GUI components */
+
+ private val graphview = new JPanel
+
+ // FIXME mutable GUI content
+ private def set_graphview(graph: XML.Body)
+ {
+ graphview.removeAll()
+ graphview.setLayout(new BorderLayout)
+ val panel = new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph))
+ graphview.add(panel.peer, BorderLayout.CENTER)
+ }
+
+ set_graphview(current_graph)
+ set_content(graphview)
+
+
+ private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
+ {
+ Swing_Thread.require()
+
+ val (new_snapshot, new_state) =
+ Document_View(view.getTextArea) match {
+ case Some(doc_view) =>
+ val snapshot = doc_view.model.snapshot()
+ if (follow && !snapshot.is_outdated) {
+ snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
+ case Some(cmd) =>
+ (snapshot, snapshot.state.command_state(snapshot.version, cmd))
+ case None =>
+ (Document.State.init.snapshot(), Command.empty.init_state)
+ }
+ }
+ else (current_snapshot, current_state)
+ case None => (current_snapshot, current_state)
+ }
+
+ val new_graph =
+ if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
+ new_state.markup.cumulate[Option[XML.Body]](
+ new_state.command.range, None, Some(Set(Isabelle_Markup.GRAPHVIEW)),
+ {
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.GRAPHVIEW, _), graph))) =>
+ Some(graph)
+ }).filter(_.info.isDefined) match {
+ case Text.Info(_, Some(graph)) #:: _ => graph
+ case _ => Nil
+ }
+ }
+ else current_graph
+
+ if (new_graph != current_graph) set_graphview(new_graph)
+
+ current_snapshot = new_snapshot
+ current_state = new_state
+ current_graph = new_graph
+ }
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case Session.Global_Options => // FIXME
+
+ case changed: Session.Commands_Changed =>
+ Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
+
+ case Session.Caret_Focus =>
+ Swing_Thread.later { handle_update(do_update, None) }
+
+ case bad =>
+ java.lang.System.err.println("Graph_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init()
+ {
+ Swing_Thread.require()
+
+ Isabelle.session.global_options += main_actor
+ Isabelle.session.commands_changed += main_actor
+ Isabelle.session.caret_focus += main_actor
+ handle_update(do_update, None)
+ }
+
+ override def exit()
+ {
+ Swing_Thread.require()
+
+ Isabelle.session.global_options -= main_actor
+ Isabelle.session.commands_changed -= main_actor
+ Isabelle.session.caret_focus -= main_actor
+ }
+}