# HG changeset patch
# User blanchet
# Date 1355153183 -3600
# Node ID dc160c718f38ee521697c1405d480e767ebdf58d
# Parent b00823a7445056191b9a65e9030158a0f5bd3e08# Parent e732da007562b2b950fb44f967cd91930285c90c
merged
diff -r b00823a74450 -r dc160c718f38 NEWS
--- a/NEWS Mon Dec 10 16:20:04 2012 +0100
+++ b/NEWS Mon Dec 10 16:26:23 2012 +0100
@@ -72,7 +72,7 @@
* Smarter handling of tracing messages: output window informs about
accumulated messages; prover transactions are limited to emit maximum
amount of output, before being canceled (cf. system option
-"editor_tracing_limit"). This avoids swamping the front-end with
+"editor_tracing_limit_MB"). This avoids swamping the front-end with
potentially infinite message streams.
* More plugin options and preferences, based on Isabelle/Scala. The
diff -r b00823a74450 -r dc160c718f38 README_REPOSITORY
--- a/README_REPOSITORY Mon Dec 10 16:20:04 2012 +0100
+++ b/README_REPOSITORY Mon Dec 10 16:26:23 2012 +0100
@@ -1,18 +1,21 @@
Important notes on Mercurial repository access for Isabelle
===========================================================
-Quick start in 20min
+Quick start in 25min
--------------------
-1. Ensure that "hg" (Mercurial) is installed; see also
- http://www.selenic.com/mercurial
+1a. Windows: ensure that Cygwin with Mercurial and Perl is installed;
+ see also http://www.cygwin.com/
+
+1b. Mac OS X and Linux: ensure that Mercurial (hg) is installed; see
+ also http://www.selenic.com/mercurial
2. Create file $HOME/.isabelle/etc/settings and insert the following
line near its beginning:
init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
-3. Execute shell commands as follows:
+3. Execute bash shell commands as follows:
hg clone http://isabelle.in.tum.de/repos/isabelle
diff -r b00823a74450 -r dc160c718f38 etc/options
--- a/etc/options Mon Dec 10 16:20:04 2012 +0100
+++ b/etc/options Mon Dec 10 16:26:23 2012 +0100
@@ -96,5 +96,5 @@
option editor_reparse_limit : int = 10000
-- "maximum amount of reparsed text outside perspective"
-option editor_tracing_limit : int = 1000000
+option editor_tracing_limit_MB : real = 2.5
-- "maximum tracing volume for each command transaction"
diff -r b00823a74450 -r dc160c718f38 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon Dec 10 16:20:04 2012 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon Dec 10 16:26:23 2012 +0100
@@ -130,7 +130,7 @@
fun output_line cert =
"To repeat this proof with a certifiate use this command:\n" ^
- Sendback.markup ("by (sos_cert \"" ^ cert ^ "\")")
+ Active.sendback_markup ("by (sos_cert \"" ^ cert ^ "\")")
val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
diff -r b00823a74450 -r dc160c718f38 src/HOL/Statespace/StateSpaceEx.thy
--- a/src/HOL/Statespace/StateSpaceEx.thy Mon Dec 10 16:20:04 2012 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy Mon Dec 10 16:26:23 2012 +0100
@@ -235,7 +235,7 @@
ML {*
fun make_benchmark n =
- writeln (Sendback.markup
+ writeln (Active.sendback_markup
("statespace benchmark" ^ string_of_int n ^ " =\n" ^
(cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
*}
diff -r b00823a74450 -r dc160c718f38 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 10 16:20:04 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 10 16:26:23 2012 +0100
@@ -470,7 +470,8 @@
pprint_nt (fn () => Pretty.blk (0,
pstrs "Hint: To check that the induction hypothesis is \
\general enough, try this command: " @
- [Pretty.mark (Sendback.make_markup {implicit = false, properties = []})
+ [Pretty.mark
+ (Active.make_markup Markup.sendbackN {implicit = false, properties = []})
(Pretty.blk (0,
pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
else
diff -r b00823a74450 -r dc160c718f38 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Dec 10 16:20:04 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Dec 10 16:26:23 2012 +0100
@@ -829,7 +829,7 @@
(true, "")
end)
-fun sendback sub = Sendback.markup (sledgehammerN ^ " " ^ sub)
+fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
val commit_timeout = seconds 30.0
diff -r b00823a74450 -r dc160c718f38 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 10 16:20:04 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 10 16:26:23 2012 +0100
@@ -220,14 +220,14 @@
command_call (string_for_reconstructor reconstr) ss
fun try_command_line banner time command =
- banner ^ ": " ^ Sendback.markup command ^ show_time time ^ "."
+ banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
case minimize_command ss of
"" => ""
| command =>
- "\nTo minimize: " ^ Sendback.markup command ^ "."
+ "\nTo minimize: " ^ Active.sendback_markup command ^ "."
fun split_used_facts facts =
facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
@@ -728,7 +728,7 @@
in
"\n\nStructured proof "
^ (commas msg |> not (null msg) ? enclose "(" ")")
- ^ ":\n" ^ Sendback.markup isar_text
+ ^ ":\n" ^ Active.sendback_markup isar_text
end
end
val isar_proof =
diff -r b00823a74450 -r dc160c718f38 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML Mon Dec 10 16:20:04 2012 +0100
+++ b/src/HOL/Tools/try0.ML Mon Dec 10 16:26:23 2012 +0100
@@ -138,7 +138,7 @@
Auto_Try => "Auto Try Methods found a proof"
| Try => "Try Methods found a proof"
| Normal => "Try this") ^ ": " ^
- Sendback.markup
+ Active.sendback_markup
((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
"\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
diff -r b00823a74450 -r dc160c718f38 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Pure/General/graph.scala Mon Dec 10 16:26:23 2012 +0100
@@ -237,7 +237,8 @@
def transitive_reduction_acyclic: Graph[Key, A] =
{
val trans = this.transitive_closure
- assert(!trans.entries.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
+ if (trans.entries.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
+ error("Cyclic graph")
var graph = this
for {
diff -r b00823a74450 -r dc160c718f38 src/Pure/General/graph_display.ML
--- a/src/Pure/General/graph_display.ML Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Pure/General/graph_display.ML Mon Dec 10 16:26:23 2012 +0100
@@ -57,9 +57,11 @@
fun display_graph graph =
if print_mode_active graphview_reportN then
- (Output.report
- (YXML.string_of (XML.Elem ((Markup.graphviewN, []), encode_graphview graph)));
- writeln "(see graphview)")
+ let
+ val markup = Active.make_markup Markup.graphviewN {implicit = false, properties = []};
+ val ((bg1, bg2), en) = YXML.output_markup_elem markup;
+ val graph_yxml = YXML.string_of_body (encode_graphview graph);
+ in writeln ("See " ^ bg1 ^ graph_yxml ^ bg2 ^ "graphview" ^ en) end
else
let
val browser =
diff -r b00823a74450 -r dc160c718f38 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Mon Dec 10 16:26:23 2012 +0100
@@ -66,7 +66,7 @@
fun pretty_command (cmd as (name, Command {comment, ...})) =
Pretty.block
(Pretty.marks_str
- ([Sendback.make_markup {implicit = true, properties = [Markup.padding_line]},
+ ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]},
command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
diff -r b00823a74450 -r dc160c718f38 src/Pure/PIDE/active.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/active.ML Mon Dec 10 16:26:23 2012 +0100
@@ -0,0 +1,37 @@
+(* Title: Pure/PIDE/active.ML
+ Author: Makarius
+
+Active areas within the document (see also Tools/jEdit/src/active.scala).
+*)
+
+signature ACTIVE =
+sig
+ val make_markup: string -> {implicit: bool, properties: Properties.T} -> Markup.T
+ val markup_implicit: string -> string -> string
+ val markup: string -> string -> string
+ val sendback_markup_implicit: string -> string
+ val sendback_markup: string -> string
+end;
+
+structure Active: ACTIVE =
+struct
+
+fun make_markup name {implicit, properties} =
+ (name, [])
+ |> not implicit ? (fn markup =>
+ let
+ val props =
+ (case Position.get_id (Position.thread_data ()) of
+ SOME id => [(Markup.idN, id)]
+ | NONE => []);
+ in Markup.properties props markup end)
+ |> Markup.properties properties;
+
+fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
+fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
+
+val sendback_markup_implicit = markup_implicit Markup.sendbackN;
+val sendback_markup = markup Markup.sendbackN;
+
+end;
+
diff -r b00823a74450 -r dc160c718f38 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Pure/PIDE/markup.ML Mon Dec 10 16:26:23 2012 +0100
@@ -98,7 +98,8 @@
val subgoalN: string val subgoal: T
val paddingN: string
val padding_line: string * string
- val sendbackN: string val sendback: T
+ val sendbackN: string
+ val graphviewN: string
val intensifyN: string val intensify: T
val taskN: string
val acceptedN: string val accepted: T
@@ -120,7 +121,6 @@
val reportN: string val report: T
val no_reportN: string val no_report: T
val badN: string val bad: T
- val graphviewN: string
val functionN: string
val assign_execs: Properties.T
val removed_versions: Properties.T
@@ -337,9 +337,14 @@
val (stateN, state) = markup_elem "state";
val (subgoalN, subgoal) = markup_elem "subgoal";
+
+(* active areads *)
+
+val sendbackN = "sendback";
+val graphviewN = "graphview";
+
val paddingN = "padding";
val padding_line = (paddingN, lineN);
-val (sendbackN, sendback) = markup_elem "sendback";
val (intensifyN, intensify) = markup_elem "intensify";
@@ -376,8 +381,6 @@
val (badN, bad) = markup_elem "bad";
-val graphviewN = "graphview";
-
(* protocol message functions *)
diff -r b00823a74450 -r dc160c718f38 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Pure/PIDE/markup.scala Mon Dec 10 16:26:23 2012 +0100
@@ -212,9 +212,14 @@
val STATE = "state"
val SUBGOAL = "subgoal"
+
+ /* active areas */
+
+ val SENDBACK = "sendback"
+ val GRAPHVIEW = "graphview"
+
val PADDING = "padding"
val PADDING_LINE = (PADDING, LINE)
- val SENDBACK = "sendback"
val INTENSIFY = "intensify"
@@ -280,8 +285,6 @@
val BAD = "bad"
- val GRAPHVIEW = "graphview"
-
/* protocol message functions */
diff -r b00823a74450 -r dc160c718f38 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Dec 10 16:26:23 2012 +0100
@@ -118,10 +118,12 @@
/* result messages */
+ private val clean = Set(Markup.REPORT, Markup.NO_REPORT)
+
def clean_message(body: XML.Body): XML.Body =
body filter {
- case XML.Elem(Markup(Markup.REPORT, _), _) => false
- case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false
+ case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean(name)
+ case XML.Elem(Markup(name, _), _) => !clean(name)
case _ => true
} map {
case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
@@ -131,6 +133,8 @@
def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
body flatMap {
+ case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
+ List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
diff -r b00823a74450 -r dc160c718f38 src/Pure/PIDE/sendback.ML
--- a/src/Pure/PIDE/sendback.ML Mon Dec 10 16:20:04 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: Pure/PIDE/sendback.ML
- Author: Makarius
-
-Clickable "sendback" areas within the source text (see also
-Tools/jEdit/src/sendback.scala).
-*)
-
-signature SENDBACK =
-sig
- val make_markup: {implicit: bool, properties: Properties.T} -> Markup.T
- val markup_implicit: string -> string
- val markup: string -> string
-end;
-
-structure Sendback: SENDBACK =
-struct
-
-fun make_markup {implicit, properties} =
- Markup.sendback
- |> not implicit ? (fn markup =>
- let
- val props =
- (case Position.get_id (Position.thread_data ()) of
- SOME id => [(Markup.idN, id)]
- | NONE => []);
- in Markup.properties props markup end)
- |> Markup.properties properties;
-
-fun markup_implicit s = Markup.markup (make_markup {implicit = true, properties = []}) s;
-fun markup s = Markup.markup (make_markup {implicit = false, properties = []}) s;
-
-end;
-
diff -r b00823a74450 -r dc160c718f38 src/Pure/ROOT
--- a/src/Pure/ROOT Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Pure/ROOT Mon Dec 10 16:26:23 2012 +0100
@@ -144,11 +144,11 @@
"ML/ml_statistics_polyml-5.5.0.ML"
"ML/ml_syntax.ML"
"ML/ml_thms.ML"
+ "PIDE/active.ML"
"PIDE/command.ML"
"PIDE/document.ML"
"PIDE/markup.ML"
"PIDE/protocol.ML"
- "PIDE/sendback.ML"
"PIDE/xml.ML"
"PIDE/yxml.ML"
"Proof/extraction.ML"
diff -r b00823a74450 -r dc160c718f38 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Pure/ROOT.ML Mon Dec 10 16:26:23 2012 +0100
@@ -63,7 +63,7 @@
use "PIDE/xml.ML";
use "PIDE/yxml.ML";
-use "PIDE/sendback.ML";
+use "PIDE/active.ML";
use "General/graph.ML";
diff -r b00823a74450 -r dc160c718f38 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML Mon Dec 10 16:26:23 2012 +0100
@@ -224,7 +224,8 @@
then Multithreading.max_threads := 2 else ();
Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0);
Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
- tracing_limit := Options.int options "editor_tracing_limit"
+ tracing_limit :=
+ Real.round (Options.real options "editor_tracing_limit_MB" * 1024.0 * 1024.0)
end);
end;
diff -r b00823a74450 -r dc160c718f38 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Tools/jEdit/etc/options Mon Dec 10 16:26:23 2012 +0100
@@ -41,8 +41,8 @@
option quoted_color : string = "8B8B8B19"
option highlight_color : string = "50505032"
option hyperlink_color : string = "000000FF"
-option sendback_color : string = "DCDCDCFF"
-option sendback_active_color : string = "9DC75DFF"
+option active_color : string = "DCDCDCFF"
+option active_hover_color : string = "9DC75DFF"
option keyword1_color : string = "006699FF"
option keyword2_color : string = "009966FF"
diff -r b00823a74450 -r dc160c718f38 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Dec 10 16:26:23 2012 +0100
@@ -8,6 +8,7 @@
## sources
declare -a SOURCES=(
+ "src/active.scala"
"src/dockable.scala"
"src/document_model.scala"
"src/document_view.scala"
@@ -35,7 +36,6 @@
"src/rendering.scala"
"src/rich_text_area.scala"
"src/scala_console.scala"
- "src/sendback.scala"
"src/symbols_dockable.scala"
"src/syslog_dockable.scala"
"src/text_overview.scala"
diff -r b00823a74450 -r dc160c718f38 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Mon Dec 10 16:26:23 2012 +0100
@@ -29,7 +29,6 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
plugin.isabelle.jedit.Plugin.menu= \
- isabelle.graphview-panel \
isabelle.monitor-panel \
isabelle.output-panel \
isabelle.protocol-panel \
@@ -38,7 +37,6 @@
isabelle.symbols-panel \
isabelle.syslog-panel \
isabelle.theories-panel
-isabelle.graphview-panel.label=Graphview panel
isabelle.monitor-panel.label=Monitor panel
isabelle.output-panel.label=Output panel
isabelle.protocol-panel.label=Protocol panel
diff -r b00823a74450 -r dc160c718f38 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Tools/jEdit/src/actions.xml Mon Dec 10 16:26:23 2012 +0100
@@ -22,11 +22,6 @@
wm.addDockableWindow("isabelle-output");
-
-
- wm.addDockableWindow("isabelle-graphview");
-
-
wm.addDockableWindow("isabelle-raw-output");
diff -r b00823a74450 -r dc160c718f38 src/Tools/jEdit/src/active.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/active.scala Mon Dec 10 16:26:23 2012 +0100
@@ -0,0 +1,77 @@
+/* Title: Tools/jEdit/src/active.scala
+ Author: Makarius
+
+Active areas within the document.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.View
+
+
+object Active
+{
+ def action(view: View, text: String, elem: XML.Elem)
+ {
+ Swing_Thread.require()
+
+ Document_View(view.getTextArea) match {
+ case Some(doc_view) =>
+ doc_view.rich_text_area.robust_body() {
+ val text_area = doc_view.text_area
+ val model = doc_view.model
+ val buffer = model.buffer
+ val snapshot = model.snapshot()
+
+ def try_replace_command(exec_id: Document.ID, s: String)
+ {
+ snapshot.state.execs.get(exec_id).map(_.command) match {
+ case Some(command) =>
+ snapshot.node.command_start(command) match {
+ case Some(start) =>
+ JEdit_Lib.buffer_edit(buffer) {
+ buffer.remove(start, command.proper_range.length)
+ buffer.insert(start, s)
+ }
+ case None =>
+ }
+ case None =>
+ }
+ }
+
+ if (!snapshot.is_outdated) {
+ elem match {
+ case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
+ props match {
+ case Position.Id(exec_id) =>
+ try_replace_command(exec_id, text)
+ case _ =>
+ if (props.exists(_ == Markup.PADDING_LINE))
+ Isabelle.insert_line_padding(text_area, text)
+ else text_area.setSelectedText(text)
+ }
+
+ case XML.Elem(Markup(Markup.GRAPHVIEW, Position.Id(exec_id)), body) =>
+ try_replace_command(exec_id, "")
+ default_thread_pool.submit(() =>
+ {
+ val graph =
+ Exn.capture {
+ isabelle.graphview.Model.decode_graph(body)
+ .transitive_reduction_acyclic
+ }
+ Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
+ })
+
+ case _ =>
+ }
+ }
+ }
+ case None =>
+ }
+ }
+}
+
diff -r b00823a74450 -r dc160c718f38 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Dec 10 16:26:23 2012 +0100
@@ -1,8 +1,7 @@
/* Title: Tools/jEdit/src/graphview_dockable.scala
- Author: Markus Kaiser, TU Muenchen
Author: Makarius
-Dockable window for graphview.
+Stateless dockable window for graphview.
*/
package isabelle.jedit
@@ -10,133 +9,79 @@
import isabelle._
-import java.awt.BorderLayout
-import javax.swing.{JPanel, JComponent}
-
-import scala.actors.Actor._
+import javax.swing.JComponent
+import java.awt.event.{WindowFocusListener, WindowEvent}
import org.gjt.sp.jedit.View
+import scala.swing.TextArea
+
+
+object Graphview_Dockable
+{
+ /* implicit arguments -- owned by Swing thread */
+
+ private var implicit_snapshot = Document.State.init.snapshot()
+
+ private val no_graph: Exn.Result[graphview.Model.Graph] = Exn.Exn(ERROR("No graph"))
+ private var implicit_graph = no_graph
+
+ private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
+ {
+ Swing_Thread.require()
+
+ implicit_snapshot = snapshot
+ implicit_graph = graph
+ }
+
+ private def reset_implicit(): Unit =
+ set_implicit(Document.State.init.snapshot(), no_graph)
+
+ def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
+ {
+ set_implicit(snapshot, graph)
+ view.getDockableWindowManager.floatDockableWindow("isabelle-graphview")
+ }
+}
+
class Graphview_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(snapshot: Document.Snapshot, graph_xml: XML.Body)
- {
- val graph = isabelle.graphview.Model.decode_graph(graph_xml).transitive_reduction_acyclic
+ private val snapshot = Graphview_Dockable.implicit_snapshot
+ private val graph = Graphview_Dockable.implicit_graph
- graphview.removeAll()
- graphview.setLayout(new BorderLayout)
- val panel =
- new isabelle.graphview.Main_Panel(graph) {
- override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
- {
- val rendering = Rendering(snapshot, PIDE.options.value)
- new Pretty_Tooltip(view, parent, rendering, x, y, body)
- null
- }
- }
- graphview.add(panel.peer, BorderLayout.CENTER)
- graphview.revalidate()
- }
-
- set_graphview(current_snapshot, current_graph)
- set_content(graphview)
-
-
- private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
- {
- Swing_Thread.require()
+ private val window_focus_listener =
+ new WindowFocusListener {
+ def windowGainedFocus(e: WindowEvent) { Graphview_Dockable.set_implicit(snapshot, graph) }
+ def windowLostFocus(e: WindowEvent) { Graphview_Dockable.reset_implicit() }
+ }
- 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)
- }
+ val graphview =
+ graph match {
+ case Exn.Res(proper_graph) =>
+ new isabelle.graphview.Main_Panel(proper_graph) {
+ override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
+ {
+ val rendering = Rendering(snapshot, PIDE.options.value)
+ new Pretty_Tooltip(view, parent, rendering, x, y, body)
+ null
}
- 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(Markup.GRAPHVIEW)),
- {
- case (_, Text.Info(_, XML.Elem(Markup(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_snapshot, 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("Graphview_Dockable: ignoring bad message " + bad)
- }
+ case Exn.Exn(exn) => new TextArea(Exn.message(exn))
}
- }
+ set_content(graphview)
override def init()
{
Swing_Thread.require()
-
- PIDE.session.global_options += main_actor
- PIDE.session.commands_changed += main_actor
- PIDE.session.caret_focus += main_actor
- handle_update(do_update, None)
+ JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
}
override def exit()
{
Swing_Thread.require()
-
- PIDE.session.global_options -= main_actor
- PIDE.session.commands_changed -= main_actor
- PIDE.session.caret_focus -= main_actor
+ JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
}
}
diff -r b00823a74450 -r dc160c718f38 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Mon Dec 10 16:26:23 2012 +0100
@@ -36,7 +36,8 @@
implicit_info = info
}
- private def reset_implicit(): Unit = set_implicit(Document.State.init.snapshot(), Nil)
+ private def reset_implicit(): Unit =
+ set_implicit(Document.State.init.snapshot(), Nil)
def apply(view: View, snapshot: Document.Snapshot, info: XML.Body)
{
@@ -81,6 +82,22 @@
}
+ /* resize */
+
+ private val delay_resize =
+ Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+
+ addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+ })
+
+ private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
+ zoom.tooltip = "Zoom factor for basic font size"
+
+ private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
+ add(controls.peer, BorderLayout.NORTH)
+
+
/* main actor */
private val main_actor = actor {
@@ -110,23 +127,4 @@
PIDE.session.global_options -= main_actor
delay_resize.revoke()
}
-
-
- /* resize */
-
- private val delay_resize =
- Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
-
- addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
- })
-
-
- /* controls */
-
- private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
- zoom.tooltip = "Zoom factor for basic font size"
-
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
- add(controls.peer, BorderLayout.NORTH)
}
diff -r b00823a74450 -r dc160c718f38 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala Mon Dec 10 16:26:23 2012 +0100
@@ -45,7 +45,7 @@
"jedit_tooltip_font_scale", "jedit_symbols_search_limit", "jedit_tooltip_margin",
"threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
"editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
- "editor_tracing_limit", "editor_update_delay")
+ "editor_tracing_limit_MB", "editor_update_delay")
relevant_options.foreach(PIDE.options.value.check_name _)
diff -r b00823a74450 -r dc160c718f38 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Mon Dec 10 16:26:23 2012 +0100
@@ -135,8 +135,8 @@
val quoted_color = color_value("quoted_color")
val highlight_color = color_value("highlight_color")
val hyperlink_color = color_value("hyperlink_color")
- val sendback_color = color_value("sendback_color")
- val sendback_active_color = color_value("sendback_active_color")
+ val active_color = color_value("active_color")
+ val active_hover_color = color_value("active_hover_color")
val keyword1_color = color_value("keyword1_color")
val keyword2_color = color_value("keyword2_color")
@@ -249,11 +249,13 @@
}
- def sendback(range: Text.Range): Option[Text.Info[Properties.T]] =
- snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
+ private val active_include = Set(Markup.SENDBACK, Markup.GRAPHVIEW)
+
+ def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
+ snapshot.select_markup(range, Some(active_include),
{
- case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
- Text.Info(snapshot.convert(info_range), props)
+ case Text.Info(info_range, elem @ XML.Elem(markup, _))
+ if active_include(markup.name) => Text.Info(snapshot.convert(info_range), elem)
}) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
@@ -405,8 +407,8 @@
private val background1_include =
Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
- Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
- Markup.SENDBACK
+ Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
+ active_include
def background1(range: Text.Range): Stream[Text.Info[Color]] =
{
@@ -424,8 +426,8 @@
(None, Some(bad_color))
case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
(None, Some(intensify_color))
- case (_, Text.Info(_, XML.Elem(Markup(Markup.SENDBACK, _), _))) =>
- (None, Some(sendback_color))
+ case (_, Text.Info(_, XML.Elem(Markup(name, _), _))) if active_include(name) =>
+ (None, Some(active_color))
})
color <-
(result match {
diff -r b00823a74450 -r dc160c718f38 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala Mon Dec 10 16:20:04 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Dec 10 16:26:23 2012 +0100
@@ -135,10 +135,10 @@
private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _)
- private val sendback_area = new Active_Area[Properties.T]((r: Rendering) => r.sendback _)
+ private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _)
private val active_areas =
- List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
+ List((highlight_area, true), (hyperlink_area, true), (active_area, false))
def active_reset(): Unit = active_areas.foreach(_._1.reset)
private val focus_listener = new FocusAdapter {
@@ -157,8 +157,8 @@
case Some(Text.Info(_, link)) => link.follow(view)
case None =>
}
- sendback_area.text_info match {
- case Some((text, Text.Info(_, props))) => Sendback.activate(view, text, props)
+ active_area.text_info match {
+ case Some((text, Text.Info(_, markup))) => Active.action(view, text, markup)
case None =>
}
}
@@ -252,13 +252,13 @@
gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
}
- // sendback range -- potentially from other snapshot
+ // active area -- potentially from other snapshot
for {
- info <- sendback_area.info
+ info <- active_area.info
Text.Info(range, _) <- info.try_restrict(line_range)
r <- JEdit_Lib.gfx_range(text_area, range)
} {
- gfx.setColor(rendering.sendback_active_color)
+ gfx.setColor(rendering.active_hover_color)
gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
}
diff -r b00823a74450 -r dc160c718f38 src/Tools/jEdit/src/sendback.scala
--- a/src/Tools/jEdit/src/sendback.scala Mon Dec 10 16:20:04 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-/* Title: Tools/jEdit/src/sendback.scala
- Author: Makarius
-
-Clickable "sendback" areas within the source text.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.View
-
-
-object Sendback
-{
- def activate(view: View, text: String, props: Properties.T)
- {
- Swing_Thread.require()
-
- Document_View(view.getTextArea) match {
- case Some(doc_view) =>
- doc_view.rich_text_area.robust_body() {
- val text_area = doc_view.text_area
- val model = doc_view.model
- val buffer = model.buffer
- val snapshot = model.snapshot()
-
- if (!snapshot.is_outdated) {
- props match {
- case Position.Id(exec_id) =>
- snapshot.state.execs.get(exec_id).map(_.command) match {
- case Some(command) =>
- snapshot.node.command_start(command) match {
- case Some(start) =>
- JEdit_Lib.buffer_edit(buffer) {
- buffer.remove(start, command.proper_range.length)
- buffer.insert(start, text)
- }
- case None =>
- }
- case None =>
- }
- case _ =>
- if (props.exists(_ == Markup.PADDING_LINE))
- Isabelle.insert_line_padding(text_area, text)
- else text_area.setSelectedText(text)
- }
- }
- }
- case None =>
- }
- }
-}
-