# HG changeset patch # User wenzelm # Date 1375474673 -7200 # Node ID 92932931bd82ebaad12a8919e1945a386e5b1941 # Parent 4ab66773a41f513ab55644d58a9e612b522f7934 more general Output.result: allow to update arbitrary properties; clarified kind/instance of overlay GUI component, with separate output (subject to version as main Output); diff -r 4ab66773a41f -r 92932931bd82 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Fri Aug 02 22:13:31 2013 +0200 +++ b/src/Pure/General/output.ML Fri Aug 02 22:17:53 2013 +0200 @@ -35,7 +35,7 @@ val prompt_fn: (output -> unit) Unsynchronized.ref val status_fn: (output -> unit) Unsynchronized.ref val report_fn: (output -> unit) Unsynchronized.ref - val result_fn: (serial * output -> unit) Unsynchronized.ref + val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref end val urgent_message: string -> unit @@ -44,7 +44,7 @@ val prompt: string -> unit val status: string -> unit val report: string -> unit - val result: serial * string -> unit + val result: Properties.T -> string -> unit val protocol_message: Properties.T -> string -> unit val try_protocol_message: Properties.T -> string -> unit end; @@ -102,7 +102,7 @@ val prompt_fn = Unsynchronized.ref physical_stdout; val status_fn = Unsynchronized.ref (fn _: output => ()); val report_fn = Unsynchronized.ref (fn _: output => ()); - val result_fn = Unsynchronized.ref (fn _: serial * output => ()); + val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ()); val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref = Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props); end; @@ -116,7 +116,7 @@ fun prompt s = ! Internal.prompt_fn (output s); fun status s = ! Internal.status_fn (output s); fun report s = ! Internal.report_fn (output s); -fun result (i, s) = ! Internal.result_fn (i, output s); +fun result props s = ! Internal.result_fn props (output s); fun protocol_message props s = ! Internal.protocol_message_fn props (output s); fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => (); diff -r 4ab66773a41f -r 92932931bd82 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Fri Aug 02 22:13:31 2013 +0200 +++ b/src/Pure/PIDE/markup.ML Fri Aug 02 22:17:53 2013 +0200 @@ -19,6 +19,7 @@ val nameN: string val name: string -> T -> T val kindN: string + val instanceN: string val bindingN: string val binding: T val entityN: string val entity: string -> string -> T val get_entity_kind: T -> string option @@ -118,6 +119,7 @@ val finishedN: string val finished: T val failedN: string val failed: T val serialN: string + val serial_properties: int -> Properties.T val exec_idN: string val initN: string val statusN: string @@ -222,6 +224,8 @@ val kindN = "kind"; +val instanceN = "instance"; + (* formal entities *) @@ -423,6 +427,8 @@ (* messages *) val serialN = "serial"; +fun serial_properties i = [(serialN, print_int i)]; + val exec_idN = "exec_id"; val initN = "init"; diff -r 4ab66773a41f -r 92932931bd82 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Fri Aug 02 22:13:31 2013 +0200 +++ b/src/Pure/PIDE/markup.scala Fri Aug 02 22:17:53 2013 +0200 @@ -18,6 +18,9 @@ val KIND = "kind" val Kind = new Properties.String(KIND) + val INSTANCE = "instance" + val Instance = new Properties.String(INSTANCE) + /* basic markup */ diff -r 4ab66773a41f -r 92932931bd82 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Fri Aug 02 22:13:31 2013 +0200 +++ b/src/Pure/System/isabelle_process.ML Fri Aug 02 22:17:53 2013 +0200 @@ -93,6 +93,8 @@ (* output channels *) +val serial_props = Markup.serial_properties o serial; + fun init_channels channel = let val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); @@ -103,21 +105,22 @@ fun message name props body = Message_Channel.send msg_channel (Message_Channel.message name props body); - fun standard_message opt_serial name body = + fun standard_message props name body = if body = "" then () else message name - ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I) - (Position.properties_of (Position.thread_data ()))) body; + (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body; in - Output.Internal.status_fn := standard_message NONE Markup.statusN; - Output.Internal.report_fn := standard_message NONE Markup.reportN; - Output.Internal.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s); - Output.Internal.writeln_fn := (fn s => standard_message (SOME (serial ())) Markup.writelnN s); + Output.Internal.status_fn := standard_message [] Markup.statusN; + Output.Internal.report_fn := standard_message [] Markup.reportN; + Output.Internal.result_fn := + (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s); + Output.Internal.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s); Output.Internal.tracing_fn := - (fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s)); - Output.Internal.warning_fn := (fn s => standard_message (SOME (serial ())) Markup.warningN s); - Output.Internal.error_fn := (fn (i, s) => standard_message (SOME i) Markup.errorN s); + (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)); + Output.Internal.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s); + Output.Internal.error_fn := + (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s); Output.Internal.protocol_message_fn := message Markup.protocolN; Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn; Output.Internal.prompt_fn := ignore; diff -r 4ab66773a41f -r 92932931bd82 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Fri Aug 02 22:13:31 2013 +0200 +++ b/src/Pure/Tools/find_theorems.ML Fri Aug 02 22:17:53 2013 +0200 @@ -640,12 +640,15 @@ (** print function **) -val _ = Command.print_function "find_theorems" +val find_theoremsN = "find_theorems"; + +val _ = Command.print_function find_theoremsN (fn {args, ...} => - if null args then NONE - else + (case args of + [instance, query] => SOME {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn st => - writeln (cat_lines ("find_theorems" :: args))}); + Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)] query} + | _ => NONE)); end; diff -r 4ab66773a41f -r 92932931bd82 src/Tools/jEdit/src/find_dockable.scala --- a/src/Tools/jEdit/src/find_dockable.scala Fri Aug 02 22:13:31 2013 +0200 +++ b/src/Tools/jEdit/src/find_dockable.scala Fri Aug 02 22:17:53 2013 +0200 @@ -28,16 +28,15 @@ /* component state -- owned by Swing thread */ - private val identification = Document_ID.make().toString + private val FIND_THEOREMS = "find_theorems" + private val instance = Document_ID.make().toString private var zoom_factor = 100 + private var current_location: Option[Command] = None + private var current_query: String = "" private var current_snapshot = Document.State.init.snapshot() private var current_state = Command.empty.init_state private var current_output: List[XML.Tree] = Nil - private var current_location: Option[Command] = None - private var current_query: String = "" - - private val FIND_THEOREMS = "find_theorems" /* pretty text area */ @@ -54,9 +53,39 @@ (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round) } - private def handle_output() + private def handle_update() { Swing_Thread.require() + + val (new_snapshot, new_state) = + Document_View(view.getTextArea) match { + case Some(doc_view) => + val snapshot = doc_view.model.snapshot() + if (!snapshot.is_outdated) { + current_location 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_output = + (for { + (_, XML.Elem(Markup(Markup.RESULT, props), body)) <- new_state.results.entries + if props.contains((Markup.KIND, FIND_THEOREMS)) + if props.contains((Markup.INSTANCE, instance)) + } yield XML.Elem(Markup(Markup.WRITELN_MESSAGE, Nil), body)).toList + + if (new_output != current_output) + pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output)) + + current_snapshot = new_snapshot + current_state = new_state + current_output = new_output } private def clear_overlay() @@ -67,7 +96,7 @@ command <- current_location buffer <- JEdit_Lib.jedit_buffer(command.node_name.node) model <- PIDE.document_model(buffer) - } model.remove_overlay(command, FIND_THEOREMS, List(identification, current_query)) + } model.remove_overlay(command, FIND_THEOREMS, List(instance, current_query)) current_location = None current_query = "" @@ -85,7 +114,7 @@ case Some(command) => current_location = Some(command) current_query = query - doc_view.model.add_overlay(command, FIND_THEOREMS, List(identification, query)) + doc_view.model.add_overlay(command, FIND_THEOREMS, List(instance, query)) case None => } case None => @@ -120,7 +149,7 @@ case changed: Session.Commands_Changed => current_location match { case Some(command) if changed.commands.contains(command) => - Swing_Thread.later { handle_output() } + Swing_Thread.later { handle_update() } case _ => } case bad =>