--- a/NEWS Thu Dec 13 23:47:01 2012 +0100
+++ b/NEWS Fri Dec 14 12:40:07 2012 +0100
@@ -69,10 +69,9 @@
* More efficient painting and improved reactivity when editing large
files. More scalable management of formal document content.
-* 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_MB"). This avoids swamping the front-end with
+* Smarter handling of tracing messages: prover process pauses after
+certain number of messages per command transaction, with some user
+dialog to stop or continue. This avoids swamping the front-end with
potentially infinite message streams.
* More plugin options and preferences, based on Isabelle/Scala. The
--- a/etc/options Thu Dec 13 23:47:01 2012 +0100
+++ b/etc/options Fri Dec 14 12:40:07 2012 +0100
@@ -96,5 +96,5 @@
option editor_reparse_limit : int = 10000
-- "maximum amount of reparsed text outside perspective"
-option editor_tracing_limit_MB : real = 2.5
- -- "maximum tracing volume for each command transaction"
+option editor_tracing_messages : int = 100
+ -- "initial number of tracing messages for each command transaction"
--- a/src/Pure/General/output.ML Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/General/output.ML Fri Dec 14 12:40:07 2012 +0100
@@ -34,6 +34,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 protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
end
val urgent_message: string -> unit
@@ -42,8 +43,8 @@
val prompt: string -> unit
val status: string -> unit
val report: string -> unit
+ val result: serial * string -> unit
val protocol_message: Properties.T -> string -> unit
- exception TRACING_LIMIT of int
end;
structure Output: OUTPUT =
@@ -97,6 +98,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 protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode");
end;
@@ -110,10 +112,9 @@
fun prompt s = ! Private_Hooks.prompt_fn (output s);
fun status s = ! Private_Hooks.status_fn (output s);
fun report s = ! Private_Hooks.report_fn (output s);
+fun result (i, s) = ! Private_Hooks.result_fn (i, output s);
fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
-exception TRACING_LIMIT of int;
-
end;
structure Basic_Output: BASIC_OUTPUT = Output;
--- a/src/Pure/Isar/runtime.ML Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/Isar/runtime.ML Fri Dec 14 12:40:07 2012 +0100
@@ -76,7 +76,6 @@
| TOPLEVEL_ERROR => "Error"
| ERROR msg => msg
| Fail msg => raised exn "Fail" [msg]
- | Output.TRACING_LIMIT n => "Tracing limit exceeded: " ^ string_of_int n
| THEORY (msg, thys) =>
raised exn "THEORY" (msg :: map Context.str_of_thy thys)
| Ast.AST (msg, asts) =>
--- a/src/Pure/PIDE/active.ML Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/active.ML Fri Dec 14 12:40:07 2012 +0100
@@ -11,27 +11,57 @@
val markup: string -> string -> string
val sendback_markup_implicit: string -> string
val sendback_markup: string -> string
+ val dialog: unit -> (string -> Markup.T) * string future
+ val dialog_text: unit -> (string -> string) * string future
+ val dialog_result: serial -> string -> unit
end;
structure Active: ACTIVE =
struct
+(* active markup *)
+
+fun explicit_id () =
+ (case Position.get_id (Position.thread_data ()) of
+ SOME id => [(Markup.idN, id)]
+ | NONE => []);
+
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)
+ |> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup)
|> 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;
+
+(* sendback area *)
+
val sendback_markup_implicit = markup_implicit Markup.sendbackN;
val sendback_markup = markup Markup.sendbackN;
+
+(* dialog via document content *)
+
+val dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table);
+
+fun dialog () =
+ let
+ val i = serial ();
+ fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
+ val promise = Future.promise abort : string future;
+ val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
+ fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
+ in (result_markup, promise) end;
+
+fun dialog_text () =
+ let val (markup, promise) = dialog ()
+ in (fn s => Markup.markup (markup s) s, promise) end;
+
+fun dialog_result i result =
+ Synchronized.change_result dialogs
+ (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))
+ |> (fn NONE => () | SOME promise => Future.fulfill promise result);
+
end;
--- a/src/Pure/PIDE/command.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/command.scala Fri Dec 14 12:40:07 2012 +0100
@@ -17,11 +17,38 @@
{
/** accumulated results from prover **/
+ /* results */
+
+ object Results
+ {
+ val empty = new Results(SortedMap.empty)
+ def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
+ }
+
+ final class Results private(rep: SortedMap[Long, XML.Tree])
+ {
+ def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
+ def get(serial: Long): Option[XML.Tree] = rep.get(serial)
+ def entries: Iterator[(Long, XML.Tree)] = rep.iterator
+
+ def + (entry: (Long, XML.Tree)): Results =
+ if (defined(entry._1)) this
+ else new Results(rep + entry)
+
+ def ++ (other: Results): Results =
+ if (this eq other) this
+ else if (rep.isEmpty) other
+ else (this /: other.entries)(_ + _)
+ }
+
+
+ /* state */
+
sealed case class State(
- val command: Command,
- val status: List[Markup] = Nil,
- val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
- val markup: Markup_Tree = Markup_Tree.empty)
+ command: Command,
+ status: List[Markup] = Nil,
+ results: Results = Results.empty,
+ markup: Markup_Tree = Markup_Tree.empty)
{
def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
markup.to_XML(command.range, command.source, filter)
@@ -38,7 +65,8 @@
(this /: msgs)((state, msg) =>
msg match {
case elem @ XML.Elem(markup, Nil) =>
- state.add_status(markup).add_markup(Text.Info(command.proper_range, elem))
+ state.add_status(markup)
+ .add_markup(Text.Info(command.proper_range, elem)) // FIXME cumulation order!?
case _ => System.err.println("Ignored status message: " + msg); state
})
@@ -72,10 +100,10 @@
val st0 = copy(results = results + (i -> message1))
val st1 =
- if (Protocol.is_tracing(message)) st0
- else
+ if (Protocol.is_inlined(message))
(st0 /: Protocol.message_positions(command, message))(
(st, range) => st.add_markup(Text.Info(range, message2)))
+ else st0
st1
case _ => System.err.println("Ignored message without serial number: " + message); this
@@ -88,8 +116,8 @@
type Span = List[Token]
- def apply(id: Document.Command_ID, node_name: Document.Node.Name,
- span: Span, markup: Markup_Tree): Command =
+ def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span,
+ results: Results = Results.empty, markup: Markup_Tree = Markup_Tree.empty): Command =
{
val source: String =
span match {
@@ -106,21 +134,23 @@
i += n
}
- new Command(id, node_name, span1.toList, source, markup)
+ new Command(id, node_name, span1.toList, source, results, markup)
}
- val empty = Command(Document.no_id, Document.Node.Name.empty, Nil, Markup_Tree.empty)
+ val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
- def unparsed(id: Document.Command_ID, source: String, markup: Markup_Tree): Command =
- Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), markup)
+ def unparsed(id: Document.Command_ID, source: String, results: Results, markup: Markup_Tree)
+ : Command =
+ Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
- def unparsed(source: String): Command = unparsed(Document.no_id, source, Markup_Tree.empty)
+ def unparsed(source: String): Command =
+ unparsed(Document.no_id, source, Results.empty, Markup_Tree.empty)
- def rich_text(id: Document.Command_ID, body: XML.Body): Command =
+ def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command =
{
val text = XML.content(body)
val markup = Markup_Tree.from_XML(body)
- unparsed(id, text, markup)
+ unparsed(id, text, results, markup)
}
@@ -151,6 +181,7 @@
val node_name: Document.Node.Name,
val span: Command.Span,
val source: String,
+ val init_results: Command.Results,
val init_markup: Markup_Tree)
{
/* classification */
@@ -187,5 +218,6 @@
/* accumulated results */
- val init_state: Command.State = Command.State(this, markup = init_markup)
+ val init_state: Command.State =
+ Command.State(this, results = init_results, markup = init_markup)
}
--- a/src/Pure/PIDE/document.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/document.scala Fri Dec 14 12:40:07 2012 +0100
@@ -280,9 +280,9 @@
def revert(range: Text.Range): Text.Range
def eq_markup(other: Snapshot): Boolean
def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
- result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
+ result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
def select_markup[A](range: Text.Range, elements: Option[Set[String]],
- result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
+ result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
}
type Assign = List[(Document.Command_ID, Option[Document.Exec_ID])] // exec state assignment
@@ -506,29 +506,34 @@
})
def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
- result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
+ result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
{
val former_range = revert(range)
for {
(command, command_start) <- node.command_range(former_range).toStream
- Text.Info(r0, a) <- state.command_state(version, command).markup.
+ st = state.command_state(version, command)
+ res = result(st)
+ Text.Info(r0, a) <- st.markup.
cumulate[A]((former_range - command_start).restrict(command.range), info, elements,
{
case (a, Text.Info(r0, b))
- if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
- result((a, Text.Info(convert(r0 + command_start), b)))
+ if res.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
+ res((a, Text.Info(convert(r0 + command_start), b)))
})
} yield Text.Info(convert(r0 + command_start), a)
}
def select_markup[A](range: Text.Range, elements: Option[Set[String]],
- result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
+ result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
{
- val result1 =
+ def result1(st: Command.State) =
+ {
+ val res = result(st)
new PartialFunction[(Option[A], Text.Markup), Option[A]] {
- def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
- def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
+ def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = res.isDefinedAt(arg._2)
+ def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(res(arg._2))
}
+ }
for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1))
yield Text.Info(r, x)
}
--- a/src/Pure/PIDE/markup.ML Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/markup.ML Fri Dec 14 12:40:07 2012 +0100
@@ -96,11 +96,6 @@
val proof_stateN: string val proof_state: int -> T
val stateN: string val state: T
val subgoalN: string val subgoal: T
- val paddingN: string
- val padding_line: string * string
- val sendbackN: string
- val graphviewN: string
- val intensifyN: string val intensify: T
val taskN: string
val acceptedN: string val accepted: T
val forkedN: string val forked: T
@@ -111,6 +106,7 @@
val serialN: string
val initN: string
val statusN: string
+ val resultN: string
val writelnN: string
val tracingN: string
val warningN: string
@@ -121,6 +117,12 @@
val reportN: string val report: T
val no_reportN: string val no_report: T
val badN: string val bad: T
+ val intensifyN: string val intensify: T
+ val graphviewN: string
+ val sendbackN: string
+ val paddingN: string
+ val padding_line: string * string
+ val dialogN: string val dialog: serial -> string -> T
val functionN: string
val assign_execs: Properties.T
val removed_versions: Properties.T
@@ -338,17 +340,6 @@
val (subgoalN, subgoal) = markup_elem "subgoal";
-(* active areads *)
-
-val sendbackN = "sendback";
-val graphviewN = "graphview";
-
-val paddingN = "padding";
-val padding_line = (paddingN, lineN);
-
-val (intensifyN, intensify) = markup_elem "intensify";
-
-
(* command status *)
val taskN = "task";
@@ -367,6 +358,7 @@
val initN = "init";
val statusN = "status";
+val resultN = "result";
val writelnN = "writeln";
val tracingN = "tracing";
val warningN = "warning";
@@ -381,6 +373,20 @@
val (badN, bad) = markup_elem "bad";
+val (intensifyN, intensify) = markup_elem "intensify";
+
+
+(* active areas *)
+
+val graphviewN = "graphview";
+
+val sendbackN = "sendback";
+val paddingN = "padding";
+val padding_line = (paddingN, lineN);
+
+val dialogN = "dialog";
+fun dialog i result = (dialogN, [(serialN, print_int i), (resultN, result)]);
+
(* protocol message functions *)
--- a/src/Pure/PIDE/markup.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/markup.scala Fri Dec 14 12:40:07 2012 +0100
@@ -213,17 +213,6 @@
val SUBGOAL = "subgoal"
- /* active areas */
-
- val SENDBACK = "sendback"
- val GRAPHVIEW = "graphview"
-
- val PADDING = "padding"
- val PADDING_LINE = (PADDING, LINE)
-
- val INTENSIFY = "intensify"
-
-
/* command status */
val TASK = "task"
@@ -257,6 +246,7 @@
val INIT = "init"
val STATUS = "status"
val REPORT = "report"
+ val RESULT = "result"
val WRITELN = "writeln"
val TRACING = "tracing"
val WARNING = "warning"
@@ -274,8 +264,7 @@
val message: String => String =
Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
- WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
- .withDefault((name: String) => name + "_message")
+ WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE).withDefault((s: String) => s)
val Return_Code = new Properties.Int("return_code")
@@ -285,6 +274,20 @@
val BAD = "bad"
+ val INTENSIFY = "intensify"
+
+
+ /* active areas */
+
+ val GRAPHVIEW = "graphview"
+
+ val SENDBACK = "sendback"
+ val PADDING = "padding"
+ val PADDING_LINE = (PADDING, LINE)
+
+ val DIALOG = "dialog"
+ val Result = new Properties.String(RESULT)
+
/* protocol message functions */
--- a/src/Pure/PIDE/protocol.ML Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML Fri Dec 14 12:40:07 2012 +0100
@@ -60,7 +60,7 @@
|> YXML.string_of_body);
val _ = List.app Future.cancel_group (Goal.reset_futures ());
- val _ = Isabelle_Process.reset_tracing_limits ();
+ val _ = Isabelle_Process.reset_tracing ();
val _ = Document.start_execution state';
in state' end));
@@ -76,6 +76,12 @@
in state1 end));
val _ =
+ Isabelle_Process.protocol_command "Document.dialog_result"
+ (fn [serial, result] =>
+ Active.dialog_result (Markup.parse_int serial) result
+ handle exn => if Exn.is_interrupt exn then () else reraise exn);
+
+val _ =
Isabelle_Process.protocol_command "Document.invoke_scala"
(fn [id, tag, res] =>
Invoke_Scala.fulfill_method id tag res
--- a/src/Pure/PIDE/protocol.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala Fri Dec 14 12:40:07 2012 +0100
@@ -106,7 +106,7 @@
val status = command_status(st.status)
if (status.is_running) running += 1
else if (status.is_finished) {
- if (st.results.exists(p => is_warning(p._2))) warned += 1
+ if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
else finished += 1
}
else if (status.is_failed) failed += 1
@@ -145,6 +145,15 @@
/* specific messages */
+ def is_inlined(msg: XML.Tree): Boolean =
+ !(is_result(msg) || is_tracing(msg) || is_state(msg))
+
+ def is_result(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.RESULT, _), _) => true
+ case _ => false
+ }
+
def is_tracing(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Markup.TRACING, _), _) => true
@@ -152,6 +161,15 @@
case _ => false
}
+ def is_state(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.WRITELN, _),
+ List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+ case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
+ List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+ case _ => false
+ }
+
def is_warning(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Markup.WARNING, _), _) => true
@@ -166,15 +184,44 @@
case _ => false
}
- def is_state(msg: XML.Tree): Boolean =
- msg match {
- case XML.Elem(Markup(Markup.WRITELN, _),
- List(XML.Elem(Markup(Markup.STATE, _), _))) => true
- case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
- List(XML.Elem(Markup(Markup.STATE, _), _))) => true
- case _ => false
+
+ /* dialogs */
+
+ object Dialog_Args
+ {
+ def unapply(props: Properties.T): Option[(Document.ID, Long, String)] =
+ (props, props, props) match {
+ case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
+ Some((id, serial, result))
+ case _ => None
+ }
+ }
+
+ object Dialog
+ {
+ def unapply(tree: XML.Tree): Option[(Document.ID, Long, String)] =
+ tree match {
+ case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
+ Some((id, serial, result))
+ case _ => None
+ }
+ }
+
+ object Dialog_Result
+ {
+ def apply(id: Document.ID, serial: Long, result: String): XML.Elem =
+ {
+ val props = Position.Id(id) ::: Markup.Serial(serial)
+ XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
}
+ def unapply(tree: XML.Tree): Option[String] =
+ tree match {
+ case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result)
+ case _ => None
+ }
+ }
+
/* reported positions */
@@ -205,7 +252,7 @@
}
val set = positions(Set.empty, message)
- if (set.isEmpty && !is_state(message))
+ if (set.isEmpty)
set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
else set
}
@@ -269,6 +316,14 @@
}
+ /* dialog via document content */
+
+ def dialog_result(serial: Long, result: String)
+ {
+ input("Document.dialog_result", Properties.Value.Long(serial), result)
+ }
+
+
/* method invocation service */
def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
--- a/src/Pure/ROOT.ML Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/ROOT.ML Fri Dec 14 12:40:07 2012 +0100
@@ -63,7 +63,6 @@
use "PIDE/xml.ML";
use "PIDE/yxml.ML";
-use "PIDE/active.ML";
use "General/graph.ML";
@@ -99,6 +98,8 @@
use "Concurrent/mailbox.ML";
use "Concurrent/cache.ML";
+use "PIDE/active.ML";
+
(* fundamental structures *)
--- a/src/Pure/System/isabelle_process.ML Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML Fri Dec 14 12:40:07 2012 +0100
@@ -17,8 +17,8 @@
sig
val is_active: unit -> bool
val protocol_command: string -> (string list -> unit) -> unit
- val tracing_limit: int Unsynchronized.ref;
- val reset_tracing_limits: unit -> unit
+ val tracing_messages: int Unsynchronized.ref;
+ val reset_tracing: unit -> unit
val crashes: exn list Synchronized.var
val init_fifos: string -> string -> unit
val init_socket: string -> unit
@@ -63,24 +63,43 @@
end;
-(* tracing limit *)
+(* restricted tracing messages *)
-val tracing_limit = Unsynchronized.ref 1000000;
+val tracing_messages = Unsynchronized.ref 100;
-val tracing_limits = Synchronized.var "tracing_limits" (Inttab.empty: int Inttab.table);
+val command_tracing_messages =
+ Synchronized.var "command_tracing_messages" (Inttab.empty: int Inttab.table);
-fun reset_tracing_limits () = Synchronized.change tracing_limits (K Inttab.empty);
+fun reset_tracing () =
+ Synchronized.change command_tracing_messages (K Inttab.empty);
-fun update_tracing_limits msg =
+fun update_tracing () =
(case Position.get_id (Position.thread_data ()) of
NONE => ()
| SOME id =>
- Synchronized.change tracing_limits (fn tab =>
- let
- val i = Markup.parse_int id;
- val n = the_default 0 (Inttab.lookup tab i) + size msg;
- val _ = if n > ! tracing_limit then raise Output.TRACING_LIMIT n else ();
- in Inttab.update (i, n) tab end));
+ let
+ val i = Markup.parse_int id;
+ val (n, ok) =
+ Synchronized.change_result command_tracing_messages (fn tab =>
+ let
+ val n = the_default 0 (Inttab.lookup tab i) + 1;
+ val ok = n <= ! tracing_messages;
+ in ((n, ok), Inttab.update (i, n) tab) end);
+ in
+ if ok then ()
+ else
+ let
+ val (text, promise) = Active.dialog_text ();
+ val _ =
+ writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^
+ text "10" ^ ", " ^ text "100" ^ ", " ^ text "1000" ^ " messages?")
+ val m = Markup.parse_int (Future.join promise)
+ handle Fail _ => error "Stopped";
+ in
+ Synchronized.change command_tracing_messages
+ (Inttab.map_default (i, 0) (fn k => k - m))
+ end
+ end);
(* message channels *)
@@ -126,10 +145,12 @@
in
Output.Private_Hooks.status_fn := standard_message mbox NONE Markup.statusN;
Output.Private_Hooks.report_fn := standard_message mbox NONE Markup.reportN;
+ Output.Private_Hooks.result_fn :=
+ (fn (i, s) => standard_message mbox (SOME i) Markup.resultN s);
Output.Private_Hooks.writeln_fn :=
(fn s => standard_message mbox (SOME (serial ())) Markup.writelnN s);
Output.Private_Hooks.tracing_fn :=
- (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) Markup.tracingN s));
+ (fn s => (update_tracing (); standard_message mbox (SOME (serial ())) Markup.tracingN s));
Output.Private_Hooks.warning_fn :=
(fn s => standard_message mbox (SOME (serial ())) Markup.warningN s);
Output.Private_Hooks.error_fn :=
@@ -224,8 +245,7 @@
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 :=
- Real.round (Options.real options "editor_tracing_limit_MB" * 1024.0 * 1024.0)
+ tracing_messages := Options.int options "editor_tracing_messages"
end);
end;
--- a/src/Pure/System/session.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/System/session.scala Fri Dec 14 12:40:07 2012 +0100
@@ -26,6 +26,7 @@
case class Global_Options(options: Options)
case object Caret_Focus
case class Raw_Edits(edits: List[Document.Edit_Text])
+ case class Dialog_Result(id: Document.ID, serial: Long, result: String)
case class Commands_Changed(
assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
@@ -419,6 +420,10 @@
reply(())
+ case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
+ prover.get.dialog_result(serial, result)
+ handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))
+
case Messages(msgs) =>
msgs foreach {
case input: Isabelle_Process.Input =>
@@ -469,4 +474,7 @@
def update(edits: List[Document.Edit_Text])
{ session_actor !? Session.Raw_Edits(edits) }
+
+ def dialog_result(id: Document.ID, serial: Long, result: String)
+ { session_actor ! Session.Dialog_Result(id, serial, result) }
}
--- a/src/Pure/Thy/thy_syntax.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Fri Dec 14 12:40:07 2012 +0100
@@ -68,7 +68,7 @@
/* result structure */
val spans = parse_spans(syntax.scan(text))
- spans.foreach(span => add(Command(Document.no_id, node_name, span, Markup_Tree.empty)))
+ spans.foreach(span => add(Command(Document.no_id, node_name, span)))
result()
}
}
@@ -226,7 +226,7 @@
commands
case cmd :: _ =>
val hook = commands.prev(cmd)
- val inserted = spans2.map(span => Command(Document.new_id(), name, span, Markup_Tree.empty))
+ val inserted = spans2.map(span => Command(Document.new_id(), name, span))
(commands /: cmds2)(_ - _).append_after(hook, inserted)
}
}
--- a/src/Tools/jEdit/etc/options Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/etc/options Fri Dec 14 12:40:07 2012 +0100
@@ -43,6 +43,7 @@
option hyperlink_color : string = "000000FF"
option active_color : string = "DCDCDCFF"
option active_hover_color : string = "9DC75DFF"
+option active_result_color : string = "999966FF"
option keyword1_color : string = "006699FF"
option keyword2_color : string = "009966FF"
--- a/src/Tools/jEdit/src/active.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/active.scala Fri Dec 14 12:40:07 2012 +0100
@@ -44,16 +44,6 @@
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) =>
default_thread_pool.submit(() =>
{
@@ -65,7 +55,24 @@
Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
})
+ 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 _ =>
+ // FIXME pattern match problem in scala-2.9.2 (!??)
+ elem match {
+ case Protocol.Dialog(id, serial, result) =>
+ model.session.dialog_result(id, serial, result)
+
+ case _ =>
+ }
}
}
}
--- a/src/Tools/jEdit/src/graphview_dockable.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Fri Dec 14 12:40:07 2012 +0100
@@ -65,7 +65,7 @@
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)
+ new Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body)
null
}
}
--- a/src/Tools/jEdit/src/info_dockable.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Fri Dec 14 12:40:07 2012 +0100
@@ -26,22 +26,24 @@
/* implicit arguments -- owned by Swing thread */
private var implicit_snapshot = Document.State.init.snapshot()
+ private var implicit_results = Command.Results.empty
private var implicit_info: XML.Body = Nil
- private def set_implicit(snapshot: Document.Snapshot, info: XML.Body)
+ private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
{
Swing_Thread.require()
implicit_snapshot = snapshot
+ implicit_results = results
implicit_info = info
}
private def reset_implicit(): Unit =
- set_implicit(Document.State.init.snapshot(), Nil)
+ set_implicit(Document.State.init.snapshot(), Command.Results.empty, Nil)
- def apply(view: View, snapshot: Document.Snapshot, info: XML.Body)
+ def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
{
- set_implicit(snapshot, info)
+ set_implicit(snapshot, results, info)
view.getDockableWindowManager.floatDockableWindow("isabelle-info")
}
}
@@ -57,11 +59,12 @@
private var zoom_factor = 100
private val snapshot = Info_Dockable.implicit_snapshot
+ private val results = Info_Dockable.implicit_results
private val info = Info_Dockable.implicit_info
private val window_focus_listener =
new WindowFocusListener {
- def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, info) }
+ def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, results, info) }
def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() }
}
@@ -71,7 +74,7 @@
private val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
- pretty_text_area.update(snapshot, info)
+ pretty_text_area.update(snapshot, results, info)
private def handle_resize()
{
--- a/src/Tools/jEdit/src/isabelle_options.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala Fri Dec 14 12:40:07 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_MB", "editor_update_delay")
+ "editor_tracing_messages", "editor_update_delay")
relevant_options.foreach(PIDE.options.value.check_name _)
--- a/src/Tools/jEdit/src/jEdit.props Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Fri Dec 14 12:40:07 2012 +0100
@@ -191,8 +191,8 @@
isabelle.control-bold.shortcut=C+e RIGHT
isabelle.control-isub.label=Control subscript
isabelle.control-isub.shortcut=C+e DOWN
-isabelle.control-isup.label=Control superscript
-isabelle.control-isup.shortcut=C+e UP
+isabelle.control-sup.label=Control superscript
+isabelle.control-sup.shortcut=C+e UP
isabelle.control-reset.label=Control reset
isabelle.control-reset.shortcut=C+e LEFT
isabelle.decrease-font-size.label=Decrease font size
--- a/src/Tools/jEdit/src/output_dockable.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Fri Dec 14 12:40:07 2012 +0100
@@ -70,12 +70,14 @@
}
val new_output =
- if (!restriction.isDefined || restriction.get.contains(new_state.command))
- new_state.results.iterator.map(_._2).toList
+ if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
+ val rendering = Rendering(new_snapshot, PIDE.options.value)
+ rendering.output_messages(new_state)
+ }
else current_output
if (new_output != current_output)
- pretty_text_area.update(new_snapshot, Pretty.separate(new_output))
+ pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))
current_snapshot = new_snapshot
current_state = new_state
@@ -150,7 +152,8 @@
private val detach = new Button("Detach") {
reactions += {
case ButtonClicked(_) =>
- Info_Dockable(view, current_snapshot, Pretty.separate(current_output))
+ Info_Dockable(view, current_snapshot,
+ current_state.results, Pretty.separate(current_output))
}
}
detach.tooltip = "Detach window with static copy of current output"
--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Dec 14 12:40:07 2012 +0100
@@ -21,18 +21,18 @@
object Pretty_Text_Area
{
- private def text_rendering(base_snapshot: Document.Snapshot, formatted_body: XML.Body):
- (String, Rendering) =
+ private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results,
+ formatted_body: XML.Body): (String, Rendering) =
{
- val (text, state) = Pretty_Text_Area.document_state(base_snapshot, formatted_body)
+ val (text, state) = Pretty_Text_Area.document_state(base_snapshot, base_results, formatted_body)
val rendering = Rendering(state.snapshot(), PIDE.options.value)
(text, rendering)
}
- private def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body)
- : (String, Document.State) =
+ private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
+ formatted_body: XML.Body): (String, Document.State) =
{
- val command = Command.rich_text(Document.new_id(), formatted_body)
+ val command = Command.rich_text(Document.new_id(), base_results, formatted_body)
val node_name = command.node_name
val edits: List[Document.Edit_Text] =
List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
@@ -62,8 +62,9 @@
private var current_font_size: Int = 12
private var current_body: XML.Body = Nil
private var current_base_snapshot = Document.State.init.snapshot()
+ private var current_base_results = Command.Results.empty
private var current_rendering: Rendering =
- Pretty_Text_Area.text_rendering(current_base_snapshot, Nil)._2
+ Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
private val rich_text_area =
@@ -84,12 +85,14 @@
val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
val base_snapshot = current_base_snapshot
+ val base_results = current_base_results
val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
future_rendering.map(_.cancel(true))
future_rendering = Some(default_thread_pool.submit(() =>
{
- val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body)
+ val (text, rendering) =
+ Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body)
Simple_Thread.interrupted_exception()
Swing_Thread.later {
@@ -115,12 +118,13 @@
refresh()
}
- def update(base_snapshot: Document.Snapshot, body: XML.Body)
+ def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
{
Swing_Thread.require()
require(!base_snapshot.is_outdated)
current_base_snapshot = base_snapshot
+ current_base_results = base_results
current_body = body
refresh()
}
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri Dec 14 12:40:07 2012 +0100
@@ -25,7 +25,9 @@
view: View,
parent: JComponent,
rendering: Rendering,
- mouse_x: Int, mouse_y: Int, body: XML.Body)
+ mouse_x: Int, mouse_y: Int,
+ results: Command.Results,
+ body: XML.Body)
extends JWindow(JEdit_Lib.parent_window(parent) getOrElse view)
{
window =>
@@ -70,7 +72,7 @@
pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
pretty_text_area.resize(Rendering.font_family(),
Rendering.font_size("jedit_tooltip_font_scale").round)
- pretty_text_area.update(rendering.snapshot, body)
+ pretty_text_area.update(rendering.snapshot, results, body)
pretty_text_area.registerKeyboardAction(action_listener, "close_all",
KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
@@ -92,7 +94,9 @@
tooltip = "Detach tooltip window"
listenTo(mouse.clicks)
reactions += {
- case _: MouseClicked => Info_Dockable(view, rendering.snapshot, body); window.dispose()
+ case _: MouseClicked =>
+ Info_Dockable(view, rendering.snapshot, results, body)
+ window.dispose()
}
}
--- a/src/Tools/jEdit/src/rendering.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Fri Dec 14 12:40:07 2012 +0100
@@ -137,6 +137,7 @@
val hyperlink_color = color_value("hyperlink_color")
val active_color = color_value("active_color")
val active_hover_color = color_value("active_hover_color")
+ val active_result_color = color_value("active_result_color")
val keyword1_color = color_value("keyword1_color")
val keyword2_color = color_value("keyword2_color")
@@ -164,7 +165,7 @@
val results =
snapshot.cumulate_markup[(Protocol.Status, Int)](
range, (Protocol.Status.init, 0),
- Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR),
+ Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR), _ =>
{
case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
@@ -197,7 +198,7 @@
def highlight(range: Text.Range): Option[Text.Info[Color]] =
{
- snapshot.select_markup(range, Some(highlight_include),
+ snapshot.select_markup(range, Some(highlight_include), _ =>
{
case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if highlight_include(name) =>
Text.Info(snapshot.convert(info_range), highlight_color)
@@ -209,7 +210,7 @@
def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
{
- snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
+ snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include), _ =>
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
if Path.is_ok(name) =>
@@ -249,31 +250,44 @@
}
- private val active_include = Set(Markup.SENDBACK, Markup.GRAPHVIEW)
+ private val active_include = Set(Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG)
def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
- snapshot.select_markup(range, Some(active_include),
+ snapshot.select_markup(range, Some(active_include), command_state =>
{
- case Text.Info(info_range, elem @ XML.Elem(markup, _))
- if active_include(markup.name) => Text.Info(snapshot.convert(info_range), elem)
+ case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
+ if !command_state.results.defined(serial) =>
+ Text.Info(snapshot.convert(info_range), elem)
+ case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _))
+ if name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
+ Text.Info(snapshot.convert(info_range), elem)
}) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
+ def command_results(range: Text.Range): Command.Results =
+ {
+ val results =
+ snapshot.select_markup[Command.Results](range, None, command_state =>
+ { case _ => command_state.results }).map(_.info)
+ (Command.Results.empty /: results)(_ ++ _)
+ }
+
def tooltip_message(range: Text.Range): XML.Body =
{
val msgs =
- snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty,
- Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)),
- {
- case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
- if name == Markup.WRITELN ||
- name == Markup.WARNING ||
- name == Markup.ERROR =>
- msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
- case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
- if !body.isEmpty => msgs + (Document.new_id() -> msg)
- }).toList.flatMap(_.info)
- Pretty.separate(msgs.iterator.map(_._2).toList)
+ Command.Results.merge(
+ snapshot.cumulate_markup[Command.Results](range, Command.Results.empty,
+ Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
+ {
+ case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
+ if name == Markup.WRITELN ||
+ name == Markup.WARNING ||
+ name == Markup.ERROR =>
+ msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
+ case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
+ if !body.isEmpty => msgs + (Document.new_id() -> msg)
+ }).map(_.info))
+ Pretty.separate(msgs.entries.map(_._2).toList)
}
@@ -307,7 +321,7 @@
val tips =
snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
- range, Text.Info(range, Nil), Some(tooltip_elements),
+ range, Text.Info(range, Nil), Some(tooltip_elements), _ =>
{
case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
val kind1 = space_explode('_', kind).mkString(" ")
@@ -334,7 +348,7 @@
def gutter_message(range: Text.Range): Option[Icon] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)),
+ snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)), _ =>
{
case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
body match {
@@ -359,7 +373,7 @@
{
val results =
snapshot.cumulate_markup[Int](range, 0,
- Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)),
+ Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)), _ =>
{
case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
if name == Markup.WRITELN ||
@@ -385,7 +399,7 @@
def line_background(range: Text.Range): Option[(Color, Boolean)] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0, Some(messages_include),
+ snapshot.cumulate_markup[Int](range, 0, Some(messages_include), _ =>
{
case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
if name == Markup.WRITELN_MESSAGE ||
@@ -396,7 +410,7 @@
val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
val is_separator = pri > 0 &&
- snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)),
+ snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)), _ =>
{
case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => true
}).exists(_.info)
@@ -405,6 +419,12 @@
}
+ def output_messages(st: Command.State): List[XML.Tree] =
+ {
+ st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
+ }
+
+
private val background1_include =
Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
@@ -417,7 +437,7 @@
for {
Text.Info(r, result) <-
snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
- range, (Some(Protocol.Status.init), None), Some(background1_include),
+ range, (Some(Protocol.Status.init), None), Some(background1_include), command_state =>
{
case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
if (Protocol.command_status_markup(markup.name)) =>
@@ -426,7 +446,19 @@
(None, Some(bad_color))
case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
(None, Some(intensify_color))
- case (_, Text.Info(_, XML.Elem(Markup(name, _), _))) if active_include(name) =>
+ case (acc, Text.Info(_, elem @ XML.Elem(Markup(Markup.DIALOG, _), _))) =>
+ // FIXME pattern match problem in scala-2.9.2 (!??)
+ elem match {
+ case Protocol.Dialog(_, serial, result) =>
+ command_state.results.get(serial) match {
+ case Some(Protocol.Dialog_Result(res)) if res == result =>
+ (None, Some(active_result_color))
+ case _ =>
+ (None, Some(active_color))
+ }
+ case _ => acc
+ }
+ case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) =>
(None, Some(active_color))
})
color <-
@@ -442,14 +474,14 @@
def background2(range: Text.Range): Stream[Text.Info[Color]] =
- snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)),
+ snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
{
case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
})
def foreground(range: Text.Range): Stream[Text.Info[Color]] =
- snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)),
+ snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)), _ =>
{
case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
@@ -489,7 +521,7 @@
{
if (color == Token_Markup.hidden_color) Stream(Text.Info(range, color))
else
- snapshot.cumulate_markup(range, color, Some(text_color_elements),
+ snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
{
case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
if text_colors.isDefinedAt(m) => text_colors(m)
--- a/src/Tools/jEdit/src/rich_text_area.scala Thu Dec 13 23:47:01 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Dec 14 12:40:07 2012 +0100
@@ -210,7 +210,8 @@
if (!tip.isEmpty) {
val painter = text_area.getPainter
val y1 = y + painter.getFontMetrics.getHeight / 2
- new Pretty_Tooltip(view, painter, rendering, x, y1, tip)
+ val results = rendering.command_results(range)
+ new Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
}
}
}