--- a/src/Pure/Concurrent/simple_thread.scala Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala Mon May 05 17:48:55 2014 +0200
@@ -16,12 +16,6 @@
object Simple_Thread
{
- /* pending interrupts */
-
- def interrupted_exception(): Unit =
- if (Thread.interrupted()) throw Exn.Interrupt()
-
-
/* plain thread */
def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
--- a/src/Pure/General/exn.scala Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/General/exn.scala Mon May 05 17:48:55 2014 +0200
@@ -45,6 +45,22 @@
def apply(): Throwable = new InterruptedException
def unapply(exn: Throwable): Boolean = is_interrupt(exn)
+ def expose() { if (Thread.interrupted()) throw apply() }
+ def impose() { Thread.currentThread.interrupt }
+
+ def postpone[A](body: => A): Option[A] =
+ {
+ val interrupted = Thread.interrupted
+ val result = capture { body }
+ if (interrupted) impose()
+ result match {
+ case Res(x) => Some(x)
+ case Exn(e) =>
+ if (is_interrupt(e)) { impose(); None }
+ else throw e
+ }
+ }
+
val return_code = 130
}
--- a/src/Pure/Isar/isar_cmd.ML Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon May 05 17:48:55 2014 +0200
@@ -35,7 +35,7 @@
val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
val diag_state: Proof.context -> Toplevel.state
val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
- val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
+ val pretty_theorems: bool -> Toplevel.state -> Pretty.T
val thy_deps: Toplevel.transition -> Toplevel.transition
val locale_deps: Toplevel.transition -> Toplevel.transition
val class_deps: Toplevel.transition -> Toplevel.transition
@@ -258,20 +258,19 @@
(Scan.succeed "Isar_Cmd.diag_goal ML_context"));
-(* print theorems *)
-
-fun print_theorems_proof verbose =
- Toplevel.keep (fn st =>
- Proof_Context.print_local_facts (Proof.context_of (Toplevel.proof_of st)) verbose);
+(* theorems of theory or proof context *)
-fun print_theorems_theory verbose = Toplevel.keep (fn state =>
- Toplevel.theory_of state |>
- (case Toplevel.previous_context_of state of
- SOME prev => Proof_Display.print_theorems_diff verbose (Proof_Context.theory_of prev)
- | NONE => Proof_Display.print_theorems verbose));
-
-fun print_theorems verbose =
- Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof verbose;
+fun pretty_theorems verbose st =
+ if Toplevel.is_proof st then
+ Pretty.chunks (Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose)
+ else
+ let
+ val thy = Toplevel.theory_of st;
+ val prev_thys =
+ (case Toplevel.previous_context_of st of
+ SOME prev => [Proof_Context.theory_of prev]
+ | NONE => Theory.parents_of thy);
+ in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
(* display dependencies *)
--- a/src/Pure/Isar/isar_syn.ML Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon May 05 17:48:55 2014 +0200
@@ -673,32 +673,36 @@
val _ =
Outer_Syntax.command @{command_spec "qed"} "conclude proof"
- (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Isar_Cmd.qed m)));
+ (Scan.option Method.parse >> (fn m =>
+ (Option.map Method.report m;
+ Toplevel.print o Isar_Cmd.qed m)));
val _ =
Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
(Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
- (Method.report m1; Option.map Method.report m2; Isar_Cmd.terminal_proof (m1, m2))));
+ (Method.report m1;
+ Option.map Method.report m2;
+ Toplevel.print o Isar_Cmd.terminal_proof (m1, m2))));
val _ =
Outer_Syntax.command @{command_spec ".."} "default proof"
- (Scan.succeed Isar_Cmd.default_proof);
+ (Scan.succeed (Toplevel.print o Isar_Cmd.default_proof));
val _ =
Outer_Syntax.command @{command_spec "."} "immediate proof"
- (Scan.succeed Isar_Cmd.immediate_proof);
+ (Scan.succeed (Toplevel.print o Isar_Cmd.immediate_proof));
val _ =
Outer_Syntax.command @{command_spec "done"} "done proof"
- (Scan.succeed Isar_Cmd.done_proof);
+ (Scan.succeed (Toplevel.print o Isar_Cmd.done_proof));
val _ =
Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
- (Scan.succeed Isar_Cmd.skip_proof);
+ (Scan.succeed (Toplevel.print o Isar_Cmd.skip_proof));
val _ =
Outer_Syntax.command @{command_spec "oops"} "forget proof"
- (Scan.succeed Toplevel.forget_proof);
+ (Scan.succeed (Toplevel.print o Toplevel.forget_proof));
(* proof steps *)
@@ -742,7 +746,8 @@
Toplevel.skip_proof (fn h => (report_back (); h))));
-(* nested commands *)
+
+(** nested commands **)
val props_text =
Scan.optional Parse.properties [] -- Parse.position Parse.string
@@ -788,7 +793,7 @@
val _ =
Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
- (Scan.succeed (Toplevel.keep Toplevel.print_state_context));
+ (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_state_context)));
val _ =
Outer_Syntax.improper_command @{command_spec "print_theory"}
@@ -817,7 +822,8 @@
val _ =
Outer_Syntax.improper_command @{command_spec "print_theorems"}
"print theorems of local theory or proof context"
- (opt_bang >> Isar_Cmd.print_theorems);
+ (opt_bang >> (fn b =>
+ Toplevel.unknown_context o Toplevel.keep (Pretty.writeln o Isar_Cmd.pretty_theorems b)));
val _ =
Outer_Syntax.improper_command @{command_spec "print_locales"}
@@ -905,7 +911,7 @@
val _ =
Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
(Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of)));
+ Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_binds o Toplevel.context_of)));
val _ =
Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
@@ -915,7 +921,7 @@
val _ =
Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
(Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of)));
+ Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
val _ =
Outer_Syntax.improper_command @{command_spec "print_statement"}
--- a/src/Pure/Isar/proof_context.ML Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon May 05 17:48:55 2014 +0200
@@ -161,9 +161,10 @@
val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
val print_syntax: Proof.context -> unit
val print_abbrevs: Proof.context -> unit
- val print_binds: Proof.context -> unit
+ val pretty_binds: Proof.context -> Pretty.T list
+ val pretty_local_facts: Proof.context -> bool -> Pretty.T list
val print_local_facts: Proof.context -> bool -> unit
- val print_cases: Proof.context -> unit
+ val pretty_cases: Proof.context -> Pretty.T list
val debug: bool Config.T
val verbose: bool Config.T
val pretty_ctxt: Proof.context -> Pretty.T list
@@ -1265,8 +1266,6 @@
else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))]
end;
-val print_binds = Pretty.writeln_chunks o pretty_binds;
-
(* local facts *)
@@ -1332,8 +1331,6 @@
else [Pretty.big_list "cases:" (map pretty_case cases)]
end;
-val print_cases = Pretty.writeln_chunks o pretty_cases;
-
end;
--- a/src/Pure/Isar/proof_display.ML Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Isar/proof_display.ML Mon May 05 17:48:55 2014 +0200
@@ -12,8 +12,8 @@
val pp_term: theory -> term -> Pretty.T
val pp_ctyp: ctyp -> Pretty.T
val pp_cterm: cterm -> Pretty.T
- val print_theorems_diff: bool -> theory -> theory -> unit
- val print_theorems: bool -> theory -> unit
+ val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T
+ val pretty_theorems: bool -> theory -> Pretty.T
val pretty_full_theory: bool -> theory -> Pretty.T
val print_theory: theory -> unit
val string_of_rule: Proof.context -> string -> thm -> string
@@ -66,11 +66,8 @@
val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
-fun print_theorems_diff verbose prev_thy thy =
- Pretty.writeln (pretty_theorems_diff verbose [prev_thy] thy);
-
-fun pretty_theorems verbose thy = pretty_theorems_diff verbose (Theory.parents_of thy) thy;
-val print_theorems = Pretty.writeln oo pretty_theorems;
+fun pretty_theorems verbose thy =
+ pretty_theorems_diff verbose (Theory.parents_of thy) thy;
fun pretty_full_theory verbose thy =
Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
--- a/src/Pure/Isar/toplevel.ML Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML Mon May 05 17:48:55 2014 +0200
@@ -22,7 +22,8 @@
val proof_of: state -> Proof.state
val proof_position_of: state -> int
val end_theory: Position.T -> state -> theory
- val print_state_context: state -> unit
+ val pretty_state_context: state -> Pretty.T list
+ val pretty_state: bool -> state -> Pretty.T list
val print_state: bool -> state -> unit
val pretty_abstract: state -> Pretty.T
val quiet: bool Unsynchronized.ref
@@ -199,22 +200,23 @@
val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I;
-fun print_state_context state =
+fun pretty_state_context state =
(case try node_of state of
NONE => []
| SOME (Theory (gthy, _)) => pretty_context gthy
| SOME (Proof (_, (_, gthy))) => pretty_context gthy
- | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy)
- |> Pretty.writeln_chunks;
+ | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy);
-fun print_state prf_only state =
+fun pretty_state prf_only state =
(case try node_of state of
NONE => []
| SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
| SOME (Proof (prf, _)) =>
Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
- | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
- |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
+ | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
+
+fun print_state prf_only =
+ pretty_state prf_only #> Pretty.markup_chunks Markup.state #> Pretty.writeln;
fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
--- a/src/Pure/PIDE/markup.ML Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/PIDE/markup.ML Mon May 05 17:48:55 2014 +0200
@@ -183,6 +183,8 @@
val loading_theory: string -> Properties.T
val dest_loading_theory: Properties.T -> string option
val use_theories_result: string -> bool -> Properties.T
+ val print_operationsN: string
+ val print_operations: Properties.T
val simp_trace_logN: string
val simp_trace_stepN: string
val simp_trace_recurseN: string
@@ -578,6 +580,9 @@
fun use_theories_result id ok =
[("function", "use_theories_result"), ("id", id), ("ok", print_bool ok)];
+val print_operationsN = "print_operations";
+val print_operations = [(functionN, print_operationsN)];
+
(* simplifier trace *)
--- a/src/Pure/PIDE/markup.scala Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/PIDE/markup.scala Mon May 05 17:48:55 2014 +0200
@@ -459,6 +459,8 @@
}
}
+ val PRINT_OPERATIONS = "print_operations"
+
/* simplifier trace */
--- a/src/Pure/PIDE/session.scala Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/PIDE/session.scala Mon May 05 17:48:55 2014 +0200
@@ -98,6 +98,7 @@
abstract class Protocol_Handler
{
+ def start(prover: Prover): Unit = {}
def stop(prover: Prover): Unit = {}
val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
}
@@ -122,6 +123,8 @@
val (handlers2, functions2) =
try {
val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
+ new_handler.start(prover)
+
val new_functions =
for ((a, f) <- new_handler.functions.toList) yield
(a, (msg: Prover.Protocol_Output) => f(prover, msg))
--- a/src/Pure/Pure.thy Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Pure.thy Mon May 05 17:48:55 2014 +0200
@@ -108,6 +108,7 @@
ML_file "ML/ml_antiquotations.ML"
ML_file "ML/ml_thms.ML"
+ML_file "Tools/print_operation.ML"
ML_file "Isar/isar_syn.ML"
ML_file "Isar/calculation.ML"
ML_file "Tools/rail.ML"
--- a/src/Pure/System/interrupt.scala Mon May 05 10:03:43 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-/* Title: Pure/System/interrupt.scala
- Author: Makarius
-
-Support for POSIX interrupts (bypassed on Windows).
-*/
-
-package isabelle
-
-
-import sun.misc.{Signal, SignalHandler}
-
-
-object Interrupt
-{
- def handler[A](h: => Unit)(e: => A): A =
- {
- val SIGINT = new Signal("INT")
- val new_handler = new SignalHandler { def handle(s: Signal) { h } }
- val old_handler = Signal.handle(SIGINT, new_handler)
- try { e } finally { Signal.handle(SIGINT, old_handler) }
- }
-
- def exception[A](e: => A): A =
- {
- val thread = Thread.currentThread
- handler { thread.interrupt } { e }
- }
-}
-
--- a/src/Pure/System/isabelle_system.scala Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala Mon May 05 17:48:55 2014 +0200
@@ -327,13 +327,7 @@
execute(true, "/usr/bin/env", "bash", "-c", "kill -" + signal + " -" + pid).waitFor
private def kill(signal: String): Boolean =
- {
- try {
- kill_cmd(signal)
- kill_cmd("0") == 0
- }
- catch { case Exn.Interrupt() => true }
- }
+ Exn.Interrupt.postpone { kill_cmd(signal); kill_cmd("0") == 0 } getOrElse true
private def multi_kill(signal: String): Boolean =
{
@@ -341,8 +335,10 @@
var count = 10
while (running && count > 0) {
if (kill(signal)) {
- try { Thread.sleep(100) } catch { case Exn.Interrupt() => }
- count -= 1
+ Exn.Interrupt.postpone {
+ Thread.sleep(100)
+ count -= 1
+ }
}
else running = false
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/posix_interrupt.scala Mon May 05 17:48:55 2014 +0200
@@ -0,0 +1,29 @@
+/* Title: Pure/System/interrupt.scala
+ Author: Makarius
+
+Support for POSIX interrupts (bypassed on Windows).
+*/
+
+package isabelle
+
+
+import sun.misc.{Signal, SignalHandler}
+
+
+object POSIX_Interrupt
+{
+ def handler[A](h: => Unit)(e: => A): A =
+ {
+ val SIGINT = new Signal("INT")
+ val new_handler = new SignalHandler { def handle(s: Signal) { h } }
+ val old_handler = Signal.handle(SIGINT, new_handler)
+ try { e } finally { Signal.handle(SIGINT, old_handler) }
+ }
+
+ def exception[A](e: => A): A =
+ {
+ val thread = Thread.currentThread
+ handler { thread.interrupt } { e }
+ }
+}
+
--- a/src/Pure/Tools/build.scala Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/Tools/build.scala Mon May 05 17:48:55 2014 +0200
@@ -37,7 +37,7 @@
if (verbose) echo(session + ": theory " + theory)
@volatile private var is_stopped = false
- def interrupt_handler[A](e: => A): A = Interrupt.handler { is_stopped = true } { e }
+ def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
override def stopped: Boolean =
{
if (Thread.interrupted) is_stopped = true
@@ -814,7 +814,7 @@
def sleep()
{
try { Thread.sleep(500) }
- catch { case Exn.Interrupt() => Thread.currentThread.interrupt }
+ catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
}
@tailrec def loop(
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/print_operation.ML Mon May 05 17:48:55 2014 +0200
@@ -0,0 +1,84 @@
+(* Title: Pure/Tools/print_operation.ML
+ Author: Makarius
+
+Print operations as asynchronous query.
+*)
+
+
+signature PRINT_OPERATION =
+sig
+ val register: string -> string -> (Toplevel.state -> string) -> unit
+end;
+
+structure Print_Operation: PRINT_OPERATION =
+struct
+
+(* maintain print operations *)
+
+local
+
+val print_operations =
+ Synchronized.var "print_operations"
+ ([]: (string * (string * (Toplevel.state -> string))) list);
+
+fun report () =
+ Output.try_protocol_message Markup.print_operations
+ let
+ val yxml =
+ Synchronized.value print_operations
+ |> map (fn (x, (y, _)) => (x, y)) |> rev
+ |> let open XML.Encode in list (pair string string) end
+ |> YXML.string_of_body;
+ in [yxml] end;
+
+val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
+
+val _ = Session.protocol_handler "isabelle.Print_Operation$Handler";
+
+in
+
+fun register name description pr =
+ (Synchronized.change print_operations (fn tab =>
+ (if not (AList.defined (op =) tab name) then ()
+ else warning ("Redefining print operation: " ^ quote name);
+ AList.update (op =) (name, (description, pr)) tab));
+ report ());
+
+val _ =
+ Query_Operation.register "print_operation" (fn {state, args, output_result} =>
+ let
+ val [name] = args;
+ val pr =
+ (case AList.lookup (op =) (Synchronized.value print_operations) name of
+ SOME (_, pr) => pr
+ | NONE => error ("Unknown print operation: " ^ quote name));
+ val result = pr state handle Toplevel.UNDEF => error "Unknown context";
+ in output_result result end);
+
+end;
+
+
+(* common print operations *)
+
+val _ =
+ register "context" "main context"
+ (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state_context);
+
+val _ =
+ register "cases" "cases of proof context"
+ (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_cases o Toplevel.context_of);
+
+val _ =
+ register "terms" "term bindings of proof context"
+ (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_binds o Toplevel.context_of);
+
+val _ =
+ register "theorems" "theorems of local theory or proof context"
+ (Pretty.string_of o Isar_Cmd.pretty_theorems false);
+
+val _ =
+ register "state" "proof state"
+ (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state true);
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/print_operation.scala Mon May 05 17:48:55 2014 +0200
@@ -0,0 +1,43 @@
+/* Title: Pure/System/print_operation.scala
+ Author: Makarius
+
+Print operations as asynchronous query.
+*/
+
+package isabelle
+
+
+object Print_Operation
+{
+ def print_operations(session: Session): List[(String, String)] =
+ session.protocol_handler("isabelle.Print_Operation$Handler") match {
+ case Some(handler: Handler) => handler.get
+ case _ => Nil
+ }
+
+
+ /* protocol handler */
+
+ class Handler extends Session.Protocol_Handler
+ {
+ private val print_operations = Synchronized(Nil: List[(String, String)])
+
+ def get: List[(String, String)] = print_operations.value
+
+ private def put(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+ {
+ val ops =
+ {
+ import XML.Decode._
+ list(pair(string, string))(YXML.parse_body(msg.text))
+ }
+ print_operations.change(_ => ops)
+ true
+ }
+
+ override def start(prover: Prover): Unit =
+ prover.protocol_command(Markup.PRINT_OPERATIONS)
+
+ val functions = Map(Markup.PRINT_OPERATIONS -> put _)
+ }
+}
--- a/src/Pure/build-jars Mon May 05 10:03:43 2014 +0200
+++ b/src/Pure/build-jars Mon May 05 17:48:55 2014 +0200
@@ -67,7 +67,6 @@
PIDE/xml.scala
PIDE/yxml.scala
System/command_line.scala
- System/interrupt.scala
System/invoke_scala.scala
System/isabelle_charset.scala
System/isabelle_font.scala
@@ -75,6 +74,7 @@
System/isabelle_system.scala
System/options.scala
System/platform.scala
+ System/posix_interrupt.scala
System/system_channel.scala
System/utf8.scala
Thy/html.scala
@@ -89,6 +89,7 @@
Tools/keywords.scala
Tools/main.scala
Tools/ml_statistics.scala
+ Tools/print_operation.scala
Tools/simplifier_trace.scala
Tools/task_statistics.scala
library.scala
--- a/src/Tools/jEdit/src/completion_popup.scala Mon May 05 10:03:43 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon May 05 17:48:55 2014 +0200
@@ -254,7 +254,7 @@
val buffer = text_area.getBuffer
val range = item.range
- if (buffer.isEditable && range.length > 0) {
+ if (buffer.isEditable) {
JEdit_Lib.buffer_edit(buffer) {
JEdit_Lib.try_get_text(buffer, range) match {
case Some(text) if text == item.original =>
@@ -524,7 +524,7 @@
Swing_Thread.require {}
val range = item.range
- if (text_field.isEditable && range.length > 0) {
+ if (text_field.isEditable) {
val content = text_field.getText
JEdit_Lib.try_get_text(content, range) match {
case Some(text) if text == item.original =>
--- a/src/Tools/jEdit/src/find_dockable.scala Mon May 05 10:03:43 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala Mon May 05 17:48:55 2014 +0200
@@ -184,9 +184,78 @@
}
+ /* print operation */
+
+ private case class Print_Item(name: String, description: String)
+ {
+ override def toString: String = description
+ }
+
+ private val print_operation = new Find_Dockable.Operation(view)
+ {
+ /* query */
+
+ val query_operation =
+ new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
+ (snapshot, results, body) =>
+ pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+ private var _selector_item: Option[Print_Item] = None
+ private var _selector = new ComboBox[Print_Item](Nil)
+
+ private def apply_query()
+ {
+ query_operation.apply_query(List(_selector.selection.item.name))
+ }
+
+ private val query_label = new Label("Print:")
+
+ def query: JComponent = _selector.peer.asInstanceOf[JComponent]
+
+
+ /* GUI page */
+
+ private def update_selector()
+ {
+ val items = Print_Operation.print_operations(PIDE.session).map(p => Print_Item(p._1, p._2))
+ _selector =
+ new ComboBox(items) {
+ _selector_item.foreach(item => selection.item = item)
+ listenTo(selection)
+ reactions += {
+ case SelectionChanged(_) =>
+ _selector_item = Some(selection.item)
+ apply_query()
+ }
+ }
+ }
+ update_selector()
+
+ private val apply_button = new Button("Apply") {
+ tooltip = "Apply to current context"
+ reactions += { case ButtonClicked(_) => apply_query() }
+ }
+
+ private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
+
+ def select
+ {
+ update_selector()
+ control_panel.contents.clear
+ control_panel.contents ++= List(query_label, _selector, apply_button, zoom)
+ }
+
+ val page =
+ new TabbedPane.Page("Print ...", new BorderPanel {
+ add(control_panel, BorderPanel.Position.North)
+ add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+ }, "Print information from context")
+ }
+
+
/* operations */
- private val operations = List(find_theorems, find_consts)
+ private val operations = List(find_theorems, find_consts, print_operation)
private val operations_pane = new TabbedPane
{
@@ -200,7 +269,7 @@
catch { case _: IndexOutOfBoundsException => None }
private def select_operation() {
- for (op <- get_operation()) op.select
+ for (op <- get_operation()) { op.select; op.query.requestFocus }
operations_pane.revalidate
}
--- a/src/Tools/jEdit/src/pretty_text_area.scala Mon May 05 10:03:43 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon May 05 17:48:55 2014 +0200
@@ -124,7 +124,7 @@
val (text, rendering) =
try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
- Simple_Thread.interrupted_exception()
+ Exn.Interrupt.expose()
Swing_Thread.later {
current_rendering = rendering