basic integration of graphview into document model;
authorwenzelm
Tue Sep 25 22:36:06 2012 +0200 (2012-09-25 ago)
changeset 4956666cbf8bb4693
parent 49565 ea4308b7ef0f
child 49567 136dd296ba24
basic integration of graphview into document model;
added Graph_Dockable;
updated Isabelle/jEdit authors and dependencies etc.;
src/Pure/General/graph_display.ML
src/Pure/PIDE/isabelle_markup.ML
src/Pure/PIDE/isabelle_markup.scala
src/Pure/System/isabelle_process.ML
src/Tools/Graphview/src/dockable.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/dockables.xml
src/Tools/jEdit/src/graph_dockable.scala
     1.1 --- a/src/Pure/General/graph_display.ML	Tue Sep 25 20:28:47 2012 +0200
     1.2 +++ b/src/Pure/General/graph_display.ML	Tue Sep 25 22:36:06 2012 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4    val write_graph_browser: Path.T -> graph -> unit
     1.5    val browserN: string
     1.6    val graphviewN: string
     1.7 +  val graphview_reportN: string
     1.8    val display_graph: graph -> unit
     1.9  end;
    1.10  
    1.11 @@ -32,6 +33,7 @@
    1.12  
    1.13  val browserN = "browser";
    1.14  val graphviewN = "graphview";
    1.15 +val graphview_reportN = "graphview_report";
    1.16  
    1.17  fun write_graph_browser path (graph: graph) =
    1.18    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
    1.19 @@ -54,19 +56,24 @@
    1.20  (* display graph *)
    1.21  
    1.22  fun display_graph graph =
    1.23 -  let
    1.24 -    val browser =
    1.25 -      (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
    1.26 -        SOME m => m = browserN
    1.27 -      | NONE => true);
    1.28 -    val (write, tool) =
    1.29 -      if browser then (write_graph_browser, "browser") else (write_graph_graphview, "graphview");
    1.30 +  if print_mode_active graphview_reportN then
    1.31 +    Output.report
    1.32 +      (YXML.string_of (XML.Elem ((Isabelle_Markup.graphviewN, []), encode_graphview graph)))
    1.33 +  else
    1.34 +    let
    1.35 +      val browser =
    1.36 +        (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
    1.37 +          SOME m => m = browserN
    1.38 +        | NONE => true);
    1.39 +      val (write, tool) =
    1.40 +        if browser then (write_graph_browser, "browser")
    1.41 +        else (write_graph_graphview, "graphview");
    1.42  
    1.43 -    val _ = writeln "Displaying graph ...";
    1.44 -    val path = Isabelle_System.create_tmp_path "graph" "";
    1.45 -    val _ = write path graph;
    1.46 -    val _ = Isabelle_System.isabelle_tool tool ("-c " ^ File.shell_path path ^ " &");
    1.47 -  in () end;
    1.48 +      val _ = writeln "Displaying graph ...";
    1.49 +      val path = Isabelle_System.create_tmp_path "graph" "";
    1.50 +      val _ = write path graph;
    1.51 +      val _ = Isabelle_System.isabelle_tool tool ("-c " ^ File.shell_path path ^ " &");
    1.52 +    in () end;
    1.53  
    1.54  end;
    1.55  
     2.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Tue Sep 25 20:28:47 2012 +0200
     2.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Tue Sep 25 22:36:06 2012 +0200
     2.3 @@ -100,6 +100,7 @@
     2.4    val reportN: string val report: Markup.T
     2.5    val no_reportN: string val no_report: Markup.T
     2.6    val badN: string val bad: Markup.T
     2.7 +  val graphviewN: string
     2.8    val functionN: string
     2.9    val assign_execs: Properties.T
    2.10    val removed_versions: Properties.T
    2.11 @@ -296,6 +297,8 @@
    2.12  
    2.13  val (badN, bad) = markup_elem "bad";
    2.14  
    2.15 +val graphviewN = "graphview";
    2.16 +
    2.17  
    2.18  (* protocol message functions *)
    2.19  
     3.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Tue Sep 25 20:28:47 2012 +0200
     3.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Sep 25 22:36:06 2012 +0200
     3.3 @@ -254,6 +254,8 @@
     3.4  
     3.5    val BAD = "bad"
     3.6  
     3.7 +  val GRAPHVIEW = "graphview"
     3.8 +
     3.9  
    3.10    /* protocol message functions */
    3.11  
     4.1 --- a/src/Pure/System/isabelle_process.ML	Tue Sep 25 20:28:47 2012 +0200
     4.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Sep 25 22:36:06 2012 +0200
     4.3 @@ -161,6 +161,10 @@
     4.4  
     4.5  (* init *)
     4.6  
     4.7 +val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
     4.8 +val default_modes2 =
     4.9 +  [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN, Graph_Display.graphview_reportN];
    4.10 +
    4.11  fun init rendezvous = ignore (Simple_Thread.fork false (fn () =>
    4.12    let
    4.13      val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
    4.14 @@ -174,9 +178,7 @@
    4.15      val _ = Context.set_thread_data NONE;
    4.16      val _ =
    4.17        Unsynchronized.change print_mode
    4.18 -        (fn mode =>
    4.19 -          (mode @ [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN])
    4.20 -          |> fold (update op =) [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]);
    4.21 +        (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
    4.22  
    4.23      val channel = rendezvous ();
    4.24      val _ = init_channels channel;
     5.1 --- a/src/Tools/Graphview/src/dockable.scala	Tue Sep 25 20:28:47 2012 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,53 +0,0 @@
     5.4 -/*  Title:      Tools/Graphview/src/dockable.scala
     5.5 -    Author:     Markus Kaiser, TU Muenchen
     5.6 -
     5.7 -Graphview jEdit dockable.
     5.8 -*/
     5.9 -
    5.10 -package isabelle.graphview
    5.11 -
    5.12 -
    5.13 -import isabelle._
    5.14 -import isabelle.jedit._
    5.15 -
    5.16 -import scala.actors.Actor._
    5.17 -import scala.swing.{FileChooser}
    5.18 -
    5.19 -import java.io.File
    5.20 -import org.gjt.sp.jedit.View
    5.21 -
    5.22 -
    5.23 -class Graphview_Dockable(view: View, position: String)
    5.24 -extends Dockable(view, position)
    5.25 -{
    5.26 -  //FIXME: How does the xml get here?
    5.27 -  val xml: XML.Tree =
    5.28 -  try {
    5.29 -    val chooser = new FileChooser()
    5.30 -    val path: File = chooser.showOpenDialog(null) match {
    5.31 -        case FileChooser.Result.Approve =>
    5.32 -          chooser.selectedFile
    5.33 -        case _ => new File("~/local_deps.graph")
    5.34 -    }
    5.35 -    YXML.parse_body(Symbol.decode(io.Source.fromFile(path).mkString)).head
    5.36 -  } catch {
    5.37 -    case ex: Exception => System.err.println(ex.getMessage); null
    5.38 -  }
    5.39 -
    5.40 -
    5.41 -  set_content(new Main_Panel(xml))
    5.42 -
    5.43 -  /* main actor */
    5.44 -
    5.45 -  private val main_actor = actor {
    5.46 -    loop {
    5.47 -      react {
    5.48 -        case result: Isabelle_Process.Output =>
    5.49 -        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
    5.50 -      }
    5.51 -    }
    5.52 -  }
    5.53 -
    5.54 -  override def init() { }
    5.55 -  override def exit() { }
    5.56 -}
     6.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Tue Sep 25 20:28:47 2012 +0200
     6.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Sep 25 22:36:06 2012 +0200
     6.3 @@ -12,6 +12,7 @@
     6.4    "src/document_model.scala"
     6.5    "src/document_view.scala"
     6.6    "src/html_panel.scala"
     6.7 +  "src/graph_dockable.scala"
     6.8    "src/hyperlink.scala"
     6.9    "src/isabelle_encoding.scala"
    6.10    "src/isabelle_logic.scala"
    6.11 @@ -89,6 +90,7 @@
    6.12  
    6.13  BUILD_ONLY=false
    6.14  BUILD_JARS="jars"
    6.15 +FRESH_OPTION=""
    6.16  JEDIT_SESSION_DIRS=""
    6.17  JEDIT_LOGIC="$ISABELLE_LOGIC"
    6.18  JEDIT_PRINT_MODE=""
    6.19 @@ -113,6 +115,7 @@
    6.20          fi
    6.21          ;;
    6.22        f)
    6.23 +        FRESH_OPTION="-f"
    6.24          BUILD_JARS="jars_fresh"
    6.25          ;;
    6.26        j)
    6.27 @@ -162,9 +165,13 @@
    6.28  ## dependencies
    6.29  
    6.30  [ -e "$ISABELLE_HOME/Admin/build" ] && \
    6.31 -  { "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?; }
    6.32 +  {
    6.33 +    "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
    6.34 +    "$ISABELLE_TOOL" graphview -b $FRESH_OPTION || exit $?
    6.35 +  }
    6.36  
    6.37  PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
    6.38 +GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/ext/Graphview.jar"
    6.39  
    6.40  pushd "$JEDIT_HOME" >/dev/null || failed
    6.41  
    6.42 @@ -193,9 +200,12 @@
    6.43      OUTDATED=true
    6.44    else
    6.45      if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
    6.46 -      declare -a DEPS=("$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
    6.47 +      declare -a DEPS=(
    6.48 +        "$JEDIT_JAR" "${JEDIT_JARS[@]}"
    6.49 +        "$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
    6.50 +      )
    6.51      elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
    6.52 -      declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
    6.53 +      declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
    6.54      else
    6.55        declare -a DEPS=()
    6.56      fi
    6.57 @@ -247,7 +257,8 @@
    6.58  
    6.59    cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
    6.60    (
    6.61 -    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
    6.62 +    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR" \
    6.63 +      "$SCALA_HOME/lib/scala-compiler.jar"
    6.64      do
    6.65        CLASSPATH="$CLASSPATH:$JAR"
    6.66      done
     7.1 --- a/src/Tools/jEdit/src/Isabelle.props	Tue Sep 25 20:28:47 2012 +0200
     7.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Tue Sep 25 22:36:06 2012 +0200
     7.3 @@ -4,20 +4,20 @@
     7.4  
     7.5  #identification
     7.6  plugin.isabelle.jedit.Plugin.name=Isabelle
     7.7 -plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Makarius Wenzel
     7.8 -plugin.isabelle.jedit.Plugin.version=0.1.0
     7.9 -plugin.isabelle.jedit.Plugin.description=Isabelle/Isar asynchronous proof document editing
    7.10 +plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Markus Kaiser, Makarius Wenzel
    7.11 +plugin.isabelle.jedit.Plugin.version=1.0.0
    7.12 +plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE
    7.13  
    7.14  #system parameters
    7.15  plugin.isabelle.jedit.Plugin.activate=startup
    7.16  plugin.isabelle.jedit.Plugin.usePluginHome=false
    7.17  
    7.18  #dependencies
    7.19 -plugin.isabelle.jedit.Plugin.depend.0=jdk 1.6
    7.20 -plugin.isabelle.jedit.Plugin.depend.1=jedit 04.03.99.00
    7.21 -plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 4.4.1
    7.22 -plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 1.8
    7.23 -plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 0.8
    7.24 +plugin.isabelle.jedit.Plugin.depend.0=jdk 1.7
    7.25 +plugin.isabelle.jedit.Plugin.depend.1=jedit 04.05.02.00
    7.26 +plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 4.5
    7.27 +plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 1.9
    7.28 +plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.3
    7.29  
    7.30  #options
    7.31  plugin.isabelle.jedit.Plugin.option-group=isabelle-general isabelle-rendering
    7.32 @@ -40,9 +40,10 @@
    7.33  
    7.34  #menu actions
    7.35  plugin.isabelle.jedit.Plugin.menu.label=Isabelle
    7.36 -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
    7.37 +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
    7.38  isabelle.session-panel.label=Prover Session panel
    7.39  isabelle.output-panel.label=Output panel
    7.40 +isabelle.graph-panel.label=Graph panel
    7.41  isabelle.output1-panel.label=Output1 panel
    7.42  isabelle.raw-output-panel.label=Raw Output panel
    7.43  isabelle.protocol-panel.label=Protocol panel
    7.44 @@ -52,6 +53,7 @@
    7.45  #dockables
    7.46  isabelle-session.title=Prover Session
    7.47  isabelle-output.title=Output
    7.48 +isabelle-graph.title=Graph
    7.49  isabelle-output1.title=Output1
    7.50  isabelle-raw-output.title=Raw Output
    7.51  isabelle-protocol.title=Protocol
     8.1 --- a/src/Tools/jEdit/src/actions.xml	Tue Sep 25 20:28:47 2012 +0200
     8.2 +++ b/src/Tools/jEdit/src/actions.xml	Tue Sep 25 22:36:06 2012 +0200
     8.3 @@ -27,6 +27,11 @@
     8.4  			wm.addDockableWindow("isabelle-output1");
     8.5  		</CODE>
     8.6  	</ACTION>
     8.7 +	<ACTION NAME="isabelle.graph-panel">
     8.8 +		<CODE>
     8.9 +			wm.addDockableWindow("isabelle-graph");
    8.10 +		</CODE>
    8.11 +	</ACTION>
    8.12  	<ACTION NAME="isabelle.raw-output-panel">
    8.13  		<CODE>
    8.14  			wm.addDockableWindow("isabelle-raw-output");
     9.1 --- a/src/Tools/jEdit/src/dockables.xml	Tue Sep 25 20:28:47 2012 +0200
     9.2 +++ b/src/Tools/jEdit/src/dockables.xml	Tue Sep 25 22:36:06 2012 +0200
     9.3 @@ -14,6 +14,9 @@
     9.4  	<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
     9.5  		new isabelle.jedit.Output_Dockable(view, position);
     9.6  	</DOCKABLE>
     9.7 +	<DOCKABLE NAME="isabelle-graph" MOVABLE="TRUE">
     9.8 +		new isabelle.jedit.Graph_Dockable(view, position);
     9.9 +	</DOCKABLE>
    9.10  	<DOCKABLE NAME="isabelle-output1" MOVABLE="TRUE">
    9.11  		new isabelle.jedit.Output1_Dockable(view, position);
    9.12  	</DOCKABLE>
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Tools/jEdit/src/graph_dockable.scala	Tue Sep 25 22:36:06 2012 +0200
    10.3 @@ -0,0 +1,131 @@
    10.4 +/*  Title:      Tools/jEdit/src/graph_dockable.scala
    10.5 +    Author:     Markus Kaiser, TU Muenchen
    10.6 +    Author:     Makarius
    10.7 +
    10.8 +Dockable window for graphview.
    10.9 +*/
   10.10 +
   10.11 +package isabelle.jedit
   10.12 +
   10.13 +
   10.14 +import isabelle._
   10.15 +
   10.16 +import java.awt.BorderLayout
   10.17 +import javax.swing.JPanel
   10.18 +
   10.19 +import scala.actors.Actor._
   10.20 +
   10.21 +import org.gjt.sp.jedit.View
   10.22 +
   10.23 +
   10.24 +class Graph_Dockable(view: View, position: String) extends Dockable(view, position)
   10.25 +{
   10.26 +  Swing_Thread.require()
   10.27 +
   10.28 +
   10.29 +  /* component state -- owned by Swing thread */
   10.30 +
   10.31 +  private val do_update = true  // FIXME
   10.32 +
   10.33 +  private var current_snapshot = Document.State.init.snapshot()
   10.34 +  private var current_state = Command.empty.init_state
   10.35 +  private var current_graph: XML.Body = Nil
   10.36 +
   10.37 +
   10.38 +  /* GUI components */
   10.39 +
   10.40 +  private val graphview = new JPanel
   10.41 +
   10.42 +  // FIXME mutable GUI content
   10.43 +  private def set_graphview(graph: XML.Body)
   10.44 +  {
   10.45 +    graphview.removeAll()
   10.46 +    graphview.setLayout(new BorderLayout)
   10.47 +    val panel = new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph))
   10.48 +    graphview.add(panel.peer, BorderLayout.CENTER)
   10.49 +  }
   10.50 +
   10.51 +  set_graphview(current_graph)
   10.52 +  set_content(graphview)
   10.53 +
   10.54 +
   10.55 +  private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
   10.56 +  {
   10.57 +    Swing_Thread.require()
   10.58 +
   10.59 +    val (new_snapshot, new_state) =
   10.60 +      Document_View(view.getTextArea) match {
   10.61 +        case Some(doc_view) =>
   10.62 +          val snapshot = doc_view.model.snapshot()
   10.63 +          if (follow && !snapshot.is_outdated) {
   10.64 +            snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
   10.65 +              case Some(cmd) =>
   10.66 +                (snapshot, snapshot.state.command_state(snapshot.version, cmd))
   10.67 +              case None =>
   10.68 +                (Document.State.init.snapshot(), Command.empty.init_state)
   10.69 +            }
   10.70 +          }
   10.71 +          else (current_snapshot, current_state)
   10.72 +        case None => (current_snapshot, current_state)
   10.73 +      }
   10.74 +
   10.75 +    val new_graph =
   10.76 +      if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
   10.77 +        new_state.markup.cumulate[Option[XML.Body]](
   10.78 +          new_state.command.range, None, Some(Set(Isabelle_Markup.GRAPHVIEW)),
   10.79 +        {
   10.80 +          case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.GRAPHVIEW, _), graph))) =>
   10.81 +            Some(graph)
   10.82 +        }).filter(_.info.isDefined) match {
   10.83 +          case Text.Info(_, Some(graph)) #:: _ => graph
   10.84 +          case _ => Nil
   10.85 +        }
   10.86 +      }
   10.87 +      else current_graph
   10.88 +
   10.89 +    if (new_graph != current_graph) set_graphview(new_graph)
   10.90 +
   10.91 +    current_snapshot = new_snapshot
   10.92 +    current_state = new_state
   10.93 +    current_graph = new_graph
   10.94 +  }
   10.95 +
   10.96 +
   10.97 +  /* main actor */
   10.98 +
   10.99 +  private val main_actor = actor {
  10.100 +    loop {
  10.101 +      react {
  10.102 +        case Session.Global_Options =>  // FIXME
  10.103 +
  10.104 +        case changed: Session.Commands_Changed =>
  10.105 +          Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
  10.106 +
  10.107 +        case Session.Caret_Focus =>
  10.108 +          Swing_Thread.later { handle_update(do_update, None) }
  10.109 +
  10.110 +        case bad =>
  10.111 +          java.lang.System.err.println("Graph_Dockable: ignoring bad message " + bad)
  10.112 +      }
  10.113 +    }
  10.114 +  }
  10.115 +
  10.116 +  override def init()
  10.117 +  {
  10.118 +    Swing_Thread.require()
  10.119 +
  10.120 +    Isabelle.session.global_options += main_actor
  10.121 +    Isabelle.session.commands_changed += main_actor
  10.122 +    Isabelle.session.caret_focus += main_actor
  10.123 +    handle_update(do_update, None)
  10.124 +  }
  10.125 +
  10.126 +  override def exit()
  10.127 +  {
  10.128 +    Swing_Thread.require()
  10.129 +
  10.130 +    Isabelle.session.global_options -= main_actor
  10.131 +    Isabelle.session.commands_changed -= main_actor
  10.132 +    Isabelle.session.caret_focus -= main_actor
  10.133 +  }
  10.134 +}