--- a/NEWS Mon Mar 31 17:17:37 2014 +0200
+++ b/NEWS Mon Mar 31 21:15:26 2014 +0200
@@ -43,25 +43,59 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
+* Improved syntactic and semantic completion mechanism:
+
+ - No completion for Isar keywords that have already been recognized
+ by the prover, e.g. ":" within accepted Isar syntax looses its
+ meaning as abbreviation for symbol "\<in>".
+
+ - Completion context provides information about embedded languages
+ of Isabelle: keywords are only completed for outer syntax, symbols
+ or antiquotations for languages that support them. E.g. no symbol
+ completion for ML source, but within ML strings, comments,
+ antiquotations.
+
+ - Support for semantic completion based on failed name space lookup.
+ The error produced by the prover contains information about
+ alternative names that are accessible in a particular position.
+ This may be used with explicit completion (C+b) or implicit
+ completion after some delay.
+
+ - Semantic completions may get extended by appending a suffix of
+ underscores to an already recognized name, e.g. "foo_" to complete
+ "foo" or "foobar" if these are known in the context. The special
+ identifier "__" serves as a wild-card in this respect: it
+ completes to the full collection of names from the name space
+ (truncated according to the system option "completion_limit").
+
+ - Syntax completion of the editor and semantic completion of the
+ prover are merged. Since the latter requires a full round-trip of
+ document update to arrive, the default for option
+ jedit_completion_delay has been changed to 0.5s to improve the
+ user experience.
+
+ - Option jedit_completion_immediate may now get used with
+ jedit_completion_delay > 0, to complete symbol abbreviations
+ aggressively while benefiting from combined syntactic and semantic
+ completion.
+
+ - Support for simple completion templates (with single
+ place-holder), e.g. "`" for text cartouche, or "@{" for
+ antiquotation.
+
+ - Improved treatment of completion vs. various forms of jEdit text
+ selection (multiple selections, rectangular selections,
+ rectangular selection as "tall caret").
+
+ - More reliable treatment of GUI events vs. completion popups: avoid
+ loosing keystrokes with slow / remote graphics displays.
+
* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
Open text buffers take precedence over copies within the file-system.
* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
auxiliary ML files.
-* Improved completion based on context information about embedded
-languages: keywords are only completed for outer syntax, symbols or
-antiquotations for languages that support them. E.g. no symbol
-completion for ML source, but within ML strings, comments,
-antiquotations.
-
-* Semantic completions may get extended by appending a suffix of
-underscores to an already recognized name, e.g. "foo_" to complete
-"foo" or "foobar" if these are known in the context. The special
-identifier "__" serves as a wild-card in this respect: it completes to
-the full collection of names from the name space (truncated according
-to the system option "completion_limit").
-
* Document panel: simplied interaction where every single mouse click
(re)opens document via desktop environment or as jEdit buffer.
--- a/src/HOL/SPARK/Tools/spark_commands.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Mon Mar 31 21:15:26 2014 +0200
@@ -106,7 +106,7 @@
Pretty.big_list (name ^ " " ^ f status)
(Element.pretty_ctxt ctxt context' @
Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |>
- Pretty.chunks2 |> Pretty.writeln
+ Pretty.writeln_chunks2
end;
val _ =
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Mar 31 21:15:26 2014 +0200
@@ -106,7 +106,7 @@
[Pretty.str (msg ^ ":"), Pretty.str ""] @
map pretty_thm with_superfluous_assumptions @
[Pretty.str "", Pretty.str end_msg]
- end |> Pretty.chunks |> Pretty.writeln
+ end |> Pretty.writeln_chunks
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Mar 31 21:15:26 2014 +0200
@@ -505,6 +505,6 @@
let
val this_thy = @{theory}
val provers = space_implode " " (#provers (default_params this_thy []))
- in Output.protocol_message Markup.sledgehammer_provers provers end)
+ in Output.protocol_message Markup.sledgehammer_provers [provers] end)
end;
--- a/src/HOL/Tools/inductive.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/HOL/Tools/inductive.ML Mon Mar 31 21:15:26 2014 +0200
@@ -232,7 +232,7 @@
(Pretty.str "(co)inductives:" ::
map (Pretty.mark_str o #1) (Name_Space.markup_entries ctxt space (Symtab.dest infos)))),
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
- end |> Pretty.chunks |> Pretty.writeln;
+ end |> Pretty.writeln_chunks;
(* inductive info *)
--- a/src/Provers/classical.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Provers/classical.ML Mon Mar 31 21:15:26 2014 +0200
@@ -632,7 +632,7 @@
Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
Pretty.strs ("safe wrappers:" :: map #1 swrappers),
Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
- |> Pretty.chunks |> Pretty.writeln
+ |> Pretty.writeln_chunks
end;
--- a/src/Pure/Concurrent/future.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Mar 31 21:15:26 2014 +0200
@@ -56,7 +56,7 @@
val interruptible_task: ('a -> 'b) -> 'a -> 'b
val cancel_group: group -> unit
val cancel: 'a future -> unit
- val error_msg: Position.T -> (serial * string) * string option -> unit
+ val error_message: Position.T -> (serial * string) * string option -> unit
val identify_result: Position.T -> 'a Exn.result -> 'a Exn.result
type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
val default_params: params
@@ -210,7 +210,7 @@
("workers_active", Markup.print_int active),
("workers_waiting", Markup.print_int waiting)] @
ML_Statistics.get ();
- in Output.try_protocol_message (Markup.ML_statistics :: stats) "" end
+ in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end
else ();
@@ -257,7 +257,7 @@
fold (fn job => fn ok => job valid andalso ok) jobs true) ());
val _ =
if ! Multithreading.trace >= 2 then
- Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
+ Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) []
else ();
val _ = SYNCHRONIZED "finish" (fn () =>
let
@@ -434,7 +434,7 @@
(* results *)
-fun error_msg pos ((serial, msg), exec_id) =
+fun error_message pos ((serial, msg), exec_id) =
Position.setmp_thread_data pos (fn () =>
let val id = Position.get_id pos in
if is_none id orelse is_none exec_id orelse id = exec_id
--- a/src/Pure/General/output.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/General/output.ML Mon Mar 31 21:15:26 2014 +0200
@@ -25,30 +25,31 @@
val physical_stderr: output -> unit
val physical_writeln: output -> unit
exception Protocol_Message of Properties.T
+ val writelns: string list -> unit
val urgent_message: string -> unit
val error_message': serial * string -> unit
val error_message: string -> unit
val prompt: string -> unit
val status: string -> unit
- val report: string -> unit
- val result: Properties.T -> string -> unit
- val protocol_message: Properties.T -> string -> unit
- val try_protocol_message: Properties.T -> string -> unit
+ val report: string list -> unit
+ val result: Properties.T -> string list -> unit
+ val protocol_message: Properties.T -> string list -> unit
+ val try_protocol_message: Properties.T -> string list -> unit
end;
signature PRIVATE_OUTPUT =
sig
include OUTPUT
- val writeln_fn: (output -> unit) Unsynchronized.ref
- val urgent_message_fn: (output -> unit) Unsynchronized.ref
- val tracing_fn: (output -> unit) Unsynchronized.ref
- val warning_fn: (output -> unit) Unsynchronized.ref
- val error_message_fn: (serial * output -> unit) Unsynchronized.ref
+ val writeln_fn: (output list -> unit) Unsynchronized.ref
+ val urgent_message_fn: (output list -> unit) Unsynchronized.ref
+ val tracing_fn: (output list -> unit) Unsynchronized.ref
+ val warning_fn: (output list -> unit) Unsynchronized.ref
+ val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
val prompt_fn: (output -> unit) Unsynchronized.ref
- val status_fn: (output -> unit) Unsynchronized.ref
- val report_fn: (output -> unit) Unsynchronized.ref
- val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
- val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
+ val status_fn: (output list -> unit) Unsynchronized.ref
+ val report_fn: (output list -> unit) Unsynchronized.ref
+ val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
+ val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
end;
structure Output: PRIVATE_OUTPUT =
@@ -94,31 +95,32 @@
exception Protocol_Message of Properties.T;
-val writeln_fn = Unsynchronized.ref physical_writeln;
-val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s); (*Proof General legacy*)
-val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
+val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
+val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); (*Proof General legacy*)
+val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
+val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
val error_message_fn =
- Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
-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 _: Properties.T => fn _: output => ());
-val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
+ Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
+val prompt_fn = Unsynchronized.ref physical_stdout; (*Proof General legacy*)
+val status_fn = Unsynchronized.ref (fn _: output list => ());
+val report_fn = Unsynchronized.ref (fn _: output list => ());
+val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ());
+val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref =
Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
-fun writeln s = ! writeln_fn (output s);
-fun urgent_message s = ! urgent_message_fn (output s); (*Proof General legacy*)
-fun tracing s = ! tracing_fn (output s);
-fun warning s = ! warning_fn (output s);
-fun error_message' (i, s) = ! error_message_fn (i, output s);
+fun writelns ss = ! writeln_fn (map output ss);
+fun writeln s = writelns [s];
+fun urgent_message s = ! urgent_message_fn [output s]; (*Proof General legacy*)
+fun tracing s = ! tracing_fn [output s];
+fun warning s = ! warning_fn [output s];
+fun error_message' (i, s) = ! error_message_fn (i, [output s]);
fun error_message s = error_message' (serial (), s);
fun prompt s = ! prompt_fn (output s);
-fun status s = ! status_fn (output s);
-fun report s = ! report_fn (output s);
-fun result props s = ! result_fn props (output s);
-fun protocol_message props s = ! protocol_message_fn props (output s);
-fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
+fun status s = ! status_fn [output s];
+fun report ss = ! report_fn (map output ss);
+fun result props ss = ! result_fn props (map output ss);
+fun protocol_message props ss = ! protocol_message_fn props (map output ss);
+fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
end;
--- a/src/Pure/General/position.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/General/position.ML Mon Mar 31 21:15:26 2014 +0200
@@ -166,7 +166,7 @@
fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
-fun report_text pos markup txt = Output.report (reported_text pos markup txt);
+fun report_text pos markup txt = Output.report [reported_text pos markup txt];
fun report pos markup = report_text pos markup "";
type report = T * Markup.T;
@@ -174,7 +174,7 @@
val reports_text =
map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
- #> implode #> Output.report;
+ #> Output.report;
val reports = map (rpair "") #> reports_text;
--- a/src/Pure/General/pretty.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/General/pretty.ML Mon Mar 31 21:15:26 2014 +0200
@@ -45,10 +45,6 @@
val text: string -> T list
val paragraph: T list -> T
val para: string -> T
- val markup_chunks: Markup.T -> T list -> T
- val chunks: T list -> T
- val chunks2: T list -> T
- val block_enclose: T * T -> T list -> T
val quote: T -> T
val backquote: T -> T
val cartouche: T -> T
@@ -72,6 +68,12 @@
val symbolic_output: T -> Output.output
val symbolic_string_of: T -> string
val str_of: T -> string
+ val markup_chunks: Markup.T -> T list -> T
+ val chunks: T list -> T
+ val chunks2: T list -> T
+ val block_enclose: T * T -> T list -> T
+ val writeln_chunks: T list -> unit
+ val writeln_chunks2: T list -> unit
val to_ML: T -> ML_Pretty.pretty
val from_ML: ML_Pretty.pretty -> T
end;
@@ -170,17 +172,6 @@
val paragraph = markup Markup.paragraph;
val para = paragraph o text;
-fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts));
-val chunks = markup_chunks Markup.empty;
-
-fun chunks2 prts =
- (case try split_last prts of
- NONE => blk (0, [])
- | SOME (prefix, last) =>
- blk (0, maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]]));
-
-fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
-
fun quote prt = blk (1, [str "\"", prt, str "\""]);
fun backquote prt = blk (1, [str "`", prt, str "`"]);
fun cartouche prt = blk (1, [str "\\<open>", prt, str "\\<close>"]);
@@ -355,6 +346,33 @@
val str_of = Output.escape o Buffer.content o unformatted;
+(* chunks *)
+
+fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts));
+val chunks = markup_chunks Markup.empty;
+
+fun chunks2 prts =
+ (case try split_last prts of
+ NONE => blk (0, [])
+ | SOME (prefix, last) =>
+ blk (0, maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]]));
+
+fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
+
+fun string_of_text_fold prt = string_of prt |> Markup.markup Markup.text_fold;
+
+fun writeln_chunks prts =
+ Output.writelns (Library.separate "\n" (map string_of_text_fold prts));
+
+fun writeln_chunks2 prts =
+ (case try split_last prts of
+ NONE => ()
+ | SOME (prefix, last) =>
+ (map (fn prt => Markup.markup Markup.text_fold (string_of prt ^ "\n") ^ "\n") prefix @
+ [string_of_text_fold last])
+ |> Output.writelns);
+
+
(** ML toplevel pretty printing **)
--- a/src/Pure/General/symbol.scala Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/General/symbol.scala Mon Mar 31 21:15:26 2014 +0200
@@ -165,6 +165,14 @@
else index(i).chr + sym - index(i).sym
}
def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
+
+ private val hash: Int = index.toList.hashCode
+ override def hashCode: Int = hash
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Index => index.sameElements(other.index)
+ case _ => false
+ }
}
--- a/src/Pure/General/timing.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/General/timing.ML Mon Mar 31 21:15:26 2014 +0200
@@ -105,7 +105,7 @@
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
fun protocol_message props t =
- Output.try_protocol_message (props @ Markup.timing_properties t) "";
+ Output.try_protocol_message (props @ Markup.timing_properties t) [];
fun protocol props f x =
let
--- a/src/Pure/Isar/args.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/args.ML Mon Mar 31 21:15:26 2014 +0200
@@ -277,8 +277,7 @@
if Context_Position.is_visible_generic context then
((pos, Markup.operator) :: maps (Token.reports_of_value o Token.closure) args1)
|> map (fn (p, m) => Position.reported_text p m "")
- |> implode
- else "";
+ else [];
in
(case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of
(SOME x, (context', [])) =>
@@ -294,7 +293,7 @@
if null args2 then "" else ":\n " ^ space_implode " " (map Token.print args2);
in
error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
- Markup.markup_report (reported_text ()))
+ Markup.markup_report (implode (reported_text ())))
end)
end;
--- a/src/Pure/Isar/attrib.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/attrib.ML Mon Mar 31 21:15:26 2014 +0200
@@ -105,7 +105,7 @@
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
in
[Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table ctxt attribs))]
- |> Pretty.chunks |> Pretty.writeln
+ |> Pretty.writeln_chunks
end;
val attribute_space = Name_Space.space_of_table o get_attributes o Context.Proof;
--- a/src/Pure/Isar/bundle.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/bundle.ML Mon Mar 31 21:15:26 2014 +0200
@@ -134,7 +134,7 @@
Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
in
map prt_bundle (Name_Space.markup_table ctxt (get_bundles ctxt))
- end |> Pretty.chunks |> Pretty.writeln;
+ end |> Pretty.writeln_chunks;
end;
--- a/src/Pure/Isar/calculation.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/calculation.ML Mon Mar 31 21:15:26 2014 +0200
@@ -46,7 +46,7 @@
in
[Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)),
Pretty.big_list "symmetry rules:" (map pretty_thm sym)]
- end |> Pretty.chunks |> Pretty.writeln;
+ end |> Pretty.writeln_chunks;
(* access calculation *)
--- a/src/Pure/Isar/class.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/class.ML Mon Mar 31 21:15:26 2014 +0200
@@ -203,8 +203,7 @@
Sorts.all_classes algebra
|> sort (Name_Space.extern_ord ctxt class_space)
|> map prt_entry
- |> Pretty.chunks2
- |> Pretty.writeln
+ |> Pretty.writeln_chunks2
end;
--- a/src/Pure/Isar/code.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/code.ML Mon Mar 31 21:15:26 2014 +0200
@@ -1036,7 +1036,7 @@
val cases = Symtab.dest ((fst o the_cases o the_exec) thy);
val undefineds = Symtab.keys ((snd o the_cases o the_exec) thy);
in
- (Pretty.writeln o Pretty.chunks) [
+ Pretty.writeln_chunks [
Pretty.block (
Pretty.str "code equations:" :: Pretty.fbrk
:: (Pretty.fbreaks o map pretty_function) functions
--- a/src/Pure/Isar/context_rules.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/context_rules.ML Mon Mar 31 21:15:26 2014 +0200
@@ -120,7 +120,7 @@
(map_filter (fn (_, (k, th)) =>
if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE)
(sort (int_ord o pairself fst) rules));
- in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
+ in Pretty.writeln_chunks (map prt_kind rule_kinds) end;
(* access data *)
--- a/src/Pure/Isar/isar_cmd.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Mar 31 21:15:26 2014 +0200
@@ -333,7 +333,7 @@
NONE => (Theory.parents_of thy, [thy])
| SOME (xs, NONE) => (map get_theory xs, [thy])
| SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
- |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
+ |> map pretty_thm |> Pretty.writeln_chunks
end);
--- a/src/Pure/Isar/isar_syn.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Mar 31 21:15:26 2014 +0200
@@ -716,7 +716,7 @@
(* proof navigation *)
fun report_back () =
- Output.report (Markup.markup Markup.bad "Explicit backtracking");
+ Output.report [Markup.markup Markup.bad "Explicit backtracking"];
val _ =
Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
--- a/src/Pure/Isar/method.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/method.ML Mon Mar 31 21:15:26 2014 +0200
@@ -328,7 +328,7 @@
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
in
[Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table ctxt meths))]
- |> Pretty.chunks |> Pretty.writeln
+ |> Pretty.writeln_chunks
end;
fun add_method name meth comment thy = thy
--- a/src/Pure/Isar/outer_syntax.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Mon Mar 31 21:15:26 2014 +0200
@@ -219,7 +219,7 @@
dest_commands (#2 (get_syntax ()))
|> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
|> map pretty_command
- |> Pretty.chunks |> Pretty.writeln;
+ |> Pretty.writeln_chunks;
fun print_outer_syntax () =
let
@@ -231,7 +231,7 @@
[Pretty.strs ("syntax keywords:" :: map quote keywords),
Pretty.big_list "commands:" (map pretty_command cmds),
Pretty.big_list "interactive-only commands:" (map pretty_command int_cmds)]
- |> Pretty.chunks |> Pretty.writeln
+ |> Pretty.writeln_chunks
end;
--- a/src/Pure/Isar/proof_context.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Mar 31 21:15:26 2014 +0200
@@ -78,8 +78,8 @@
val read_arity: Proof.context -> xstring * string list * string -> arity
val cert_arity: Proof.context -> arity -> arity
val allow_dummies: Proof.context -> Proof.context
- val prepare_sortsT: Proof.context -> typ list -> string * typ list
- val prepare_sorts: Proof.context -> term list -> string * term list
+ val prepare_sortsT: Proof.context -> typ list -> string list * typ list
+ val prepare_sorts: Proof.context -> term list -> string list * term list
val check_tfree: Proof.context -> string * sort -> string * sort
val read_term_pattern: Proof.context -> string -> term
val read_term_schematic: Proof.context -> string -> term
@@ -691,7 +691,7 @@
| TVar (xi, raw_S) => get_sort_reports xi raw_S
| _ => I)) tys [];
- in (implode (map #2 reports), get_sort) end;
+ in (map #2 reports, get_sort) end;
fun replace_sortsT get_sort =
map_atyps
@@ -1250,7 +1250,7 @@
else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
end;
-val print_abbrevs = Pretty.writeln o Pretty.chunks o pretty_abbrevs true;
+val print_abbrevs = Pretty.writeln_chunks o pretty_abbrevs true;
(* term bindings *)
@@ -1264,7 +1264,7 @@
else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))]
end;
-val print_binds = Pretty.writeln o Pretty.chunks o pretty_binds;
+val print_binds = Pretty.writeln_chunks o pretty_binds;
(* local facts *)
@@ -1284,7 +1284,7 @@
end;
fun print_local_facts ctxt verbose =
- Pretty.writeln (Pretty.chunks (pretty_local_facts ctxt verbose));
+ Pretty.writeln_chunks (pretty_local_facts ctxt verbose);
(* local contexts *)
@@ -1331,7 +1331,7 @@
else [Pretty.big_list "cases:" (map pretty_case cases)]
end;
-val print_cases = Pretty.writeln o Pretty.chunks o pretty_cases;
+val print_cases = Pretty.writeln_chunks o pretty_cases;
end;
--- a/src/Pure/Isar/toplevel.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML Mon Mar 31 21:15:26 2014 +0200
@@ -205,7 +205,7 @@
| SOME (Theory (gthy, _)) => pretty_context gthy
| SOME (Proof (_, (_, gthy))) => pretty_context gthy
| SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy)
- |> Pretty.chunks |> Pretty.writeln;
+ |> Pretty.writeln_chunks;
fun print_state prf_only state =
(case try node_of state of
--- a/src/Pure/ML/ml_compiler_polyml.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML Mon Mar 31 21:15:26 2014 +0200
@@ -55,7 +55,7 @@
fun output () =
persistent_reports
|> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
- |> implode |> Output.report;
+ |> Output.report;
in
if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
then
--- a/src/Pure/PIDE/command.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/PIDE/command.ML Mon Mar 31 21:15:26 2014 +0200
@@ -199,7 +199,7 @@
else Runtime.exn_messages_ids exn)) ();
fun report tr m =
- Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) ();
+ Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
fun status tr m =
Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
@@ -223,7 +223,7 @@
val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
val errs = errs1 @ errs2;
- val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
+ val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
in
(case result of
NONE =>
@@ -279,7 +279,7 @@
(Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
handle exn =>
if Exn.is_interrupt exn then reraise exn
- else List.app (Future.error_msg (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
+ else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
fun print_finished (Print {print_process, ...}) = memo_finished print_process;
--- a/src/Pure/PIDE/command.scala Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/PIDE/command.scala Mon Mar 31 21:15:26 2014 +0200
@@ -225,6 +225,7 @@
}
}
+ // file name and position information, *without* persistent text
class File(val file_name: String, text: CharSequence) extends Chunk
{
val length = text.length
@@ -232,6 +233,17 @@
private val symbol_index = Symbol.Index(text)
def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
+ private val hash: Int = (file_name, length, symbol_index).hashCode
+ override def hashCode: Int = hash
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: File =>
+ hash == other.hash &&
+ file_name == other.file_name &&
+ length == other.length &&
+ symbol_index == other.symbol_index
+ case _ => false
+ }
override def toString: String = "Command.File(" + file_name + ")"
}
--- a/src/Pure/PIDE/document.scala Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/PIDE/document.scala Mon Mar 31 21:15:26 2014 +0200
@@ -46,6 +46,9 @@
/* document blobs: auxiliary files */
sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean)
+ {
+ def unchanged: Blob = copy(changed = false)
+ }
object Blobs
{
@@ -157,7 +160,7 @@
}
}
case class Clear[A, B]() extends Edit[A, B]
- case class Blob[A, B]() extends Edit[A, B]
+ case class Blob[A, B](blob: Document.Blob) extends Edit[A, B]
case class Edits[A, B](edits: List[A]) extends Edit[A, B]
case class Deps[A, B](header: Header) extends Edit[A, B]
@@ -222,7 +225,7 @@
}
final class Node private(
- val is_blob: Boolean = false,
+ val get_blob: Option[Document.Blob] = None,
val header: Node.Header = Node.bad_header("Bad theory header"),
val perspective: Node.Perspective_Command =
Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
@@ -230,13 +233,13 @@
{
def clear: Node = new Node(header = header)
- def init_blob: Node = new Node(is_blob = true)
+ def init_blob(blob: Document.Blob): Node = new Node(Some(blob.unchanged))
def update_header(new_header: Node.Header): Node =
- new Node(is_blob, new_header, perspective, _commands)
+ new Node(get_blob, new_header, perspective, _commands)
def update_perspective(new_perspective: Node.Perspective_Command): Node =
- new Node(is_blob, header, new_perspective, _commands)
+ new Node(get_blob, header, new_perspective, _commands)
def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
perspective.required == other_perspective.required &&
@@ -248,7 +251,7 @@
def update_commands(new_commands: Linear_Set[Command]): Node =
if (new_commands eq _commands.commands) this
- else new Node(is_blob, header, perspective, Node.Commands(new_commands))
+ else new Node(get_blob, header, perspective, Node.Commands(new_commands))
def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
_commands.range(i)
@@ -300,6 +303,8 @@
def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
def topological_order: List[Node.Name] = graph.topological_order
+
+ override def toString: String = topological_order.mkString("Nodes(", ",", ")")
}
--- a/src/Pure/PIDE/execution.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/PIDE/execution.ML Mon Mar 31 21:15:26 2014 +0200
@@ -122,9 +122,9 @@
Exn.Exn exn =>
(status task [Markup.failed];
status task [Markup.finished];
- Output.report (Markup.markup_only Markup.bad);
+ Output.report [Markup.markup_only Markup.bad];
if exec_id = 0 then ()
- else List.app (Future.error_msg pos) (Runtime.exn_messages_ids exn))
+ else List.app (Future.error_message pos) (Runtime.exn_messages_ids exn))
| Exn.Res _ =>
status task [Markup.finished])
in Exn.release result end);
--- a/src/Pure/PIDE/protocol.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/PIDE/protocol.ML Mon Mar 31 21:15:26 2014 +0200
@@ -85,10 +85,10 @@
val _ =
Output.protocol_message Markup.assign_update
- ((new_id, assign_update) |>
+ [(new_id, assign_update) |>
let open XML.Encode
in pair int (list (pair int (list int))) end
- |> YXML.string_of_body);
+ |> YXML.string_of_body];
in Document.start_execution state' end));
val _ =
@@ -99,7 +99,7 @@
YXML.parse_body versions_yxml |>
let open XML.Decode in list int end;
val state1 = Document.remove_versions versions state;
- val _ = Output.protocol_message Markup.removed_versions versions_yxml;
+ val _ = Output.protocol_message Markup.removed_versions [versions_yxml];
in state1 end));
val _ =
--- a/src/Pure/PIDE/protocol.scala Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala Mon Mar 31 21:15:26 2014 +0200
@@ -319,9 +319,8 @@
{
/* inlined files */
- def define_blob(blob: Document.Blob): Unit =
- protocol_command_raw(
- "Document.define_blob", Bytes(blob.bytes.sha1_digest.toString), blob.bytes)
+ def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
+ protocol_command_raw("Document.define_blob", Bytes(digest.toString), bytes)
/* commands */
--- a/src/Pure/PIDE/query_operation.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/PIDE/query_operation.ML Mon Mar 31 21:15:26 2014 +0200
@@ -20,7 +20,7 @@
SOME {delay = NONE, pri = 0, persistent = false, strict = false,
print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
let
- fun result s = Output.result [(Markup.instanceN, instance)] s;
+ fun result s = Output.result [(Markup.instanceN, instance)] [s];
fun status m = result (Markup.markup_only m);
fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
fun toplevel_error exn =
--- a/src/Pure/PIDE/resources.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/PIDE/resources.ML Mon Mar 31 21:15:26 2014 +0200
@@ -213,7 +213,7 @@
if strict then error msg
else if Context_Position.is_visible ctxt then
Output.report
- (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
+ [Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg]
else ()
end;
in path end;
--- a/src/Pure/PIDE/session.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/PIDE/session.ML Mon Mar 31 21:15:26 2014 +0200
@@ -68,13 +68,13 @@
fun protocol_handler name =
Synchronized.change protocol_handlers (fn handlers =>
- (Output.try_protocol_message (Markup.protocol_handler name) "";
+ (Output.try_protocol_message (Markup.protocol_handler name) [];
if not (member (op =) handlers name) then ()
else warning ("Redefining protocol handler: " ^ quote name);
update (op =) name handlers));
fun init_protocol_handlers () =
Synchronized.value protocol_handlers
- |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) "");
+ |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) []);
end;
--- a/src/Pure/PIDE/session.scala Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/PIDE/session.scala Mon Mar 31 21:15:26 2014 +0200
@@ -384,7 +384,7 @@
change.doc_blobs.get(digest) match {
case Some(blob) =>
global_state >> (_.define_blob(digest))
- prover.get.define_blob(blob)
+ prover.get.define_blob(digest, blob.bytes)
case None =>
System.err.println("Missing blob for SHA1 digest " + digest)
}
--- a/src/Pure/Syntax/syntax.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Syntax/syntax.ML Mon Mar 31 21:15:26 2014 +0200
@@ -575,9 +575,9 @@
in
-fun print_gram syn = Pretty.writeln (Pretty.chunks (pretty_gram syn));
-fun print_trans syn = Pretty.writeln (Pretty.chunks (pretty_trans syn));
-fun print_syntax syn = Pretty.writeln (Pretty.chunks (pretty_gram syn @ pretty_trans syn));
+fun print_gram syn = Pretty.writeln_chunks (pretty_gram syn);
+fun print_trans syn = Pretty.writeln_chunks (pretty_trans syn);
+fun print_syntax syn = Pretty.writeln_chunks (pretty_gram syn @ pretty_trans syn);
end;
--- a/src/Pure/Syntax/syntax_phases.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Mar 31 21:15:26 2014 +0200
@@ -878,7 +878,7 @@
pretty_checks "term_checks" term_checks @
pretty_checks "typ_unchecks" typ_unchecks @
pretty_checks "term_unchecks" term_unchecks
- end |> Pretty.chunks |> Pretty.writeln;
+ end |> Pretty.writeln_chunks;
local
@@ -949,11 +949,10 @@
if Position.is_reported pos then
cons (Position.reported_text pos Markup.typing
(Syntax.string_of_typ ctxt (Logic.dest_type ty)))
- else I) ps tys' []
- |> implode;
+ else I) ps tys' [];
val _ =
- if Context_Position.is_visible ctxt then Output.report (sorting_report ^ typing_report)
+ if Context_Position.is_visible ctxt then Output.report (sorting_report @ typing_report)
else ();
in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
--- a/src/Pure/System/invoke_scala.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/System/invoke_scala.ML Mon Mar 31 21:15:26 2014 +0200
@@ -30,10 +30,10 @@
fun promise_method name arg =
let
val id = new_id ();
- fun abort () = Output.protocol_message (Markup.cancel_scala id) "";
+ fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
val promise = Future.promise abort : string future;
val _ = Synchronized.change promises (Symtab.update (id, promise));
- val _ = Output.protocol_message (Markup.invoke_scala name id) arg;
+ val _ = Output.protocol_message (Markup.invoke_scala name id) [arg];
in promise end;
fun method name arg = Future.join (promise_method name arg);
--- a/src/Pure/System/isabelle_process.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/System/isabelle_process.ML Mon Mar 31 21:15:26 2014 +0200
@@ -106,7 +106,7 @@
Message_Channel.send msg_channel (Message_Channel.message name props body);
fun standard_message props name body =
- if body = "" then ()
+ if forall (fn s => s = "") body then ()
else
message name
(fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
@@ -124,7 +124,7 @@
Output.protocol_message_fn := message Markup.protocolN;
Output.urgent_message_fn := ! Output.writeln_fn;
Output.prompt_fn := ignore;
- message Markup.initN [] (Session.welcome ());
+ message Markup.initN [] [Session.welcome ()];
msg_channel
end;
--- a/src/Pure/System/message_channel.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/System/message_channel.ML Mon Mar 31 21:15:26 2014 +0200
@@ -7,7 +7,7 @@
signature MESSAGE_CHANNEL =
sig
type message
- val message: string -> Properties.T -> string -> message
+ val message: string -> Properties.T -> string list -> message
type T
val send: T -> message -> unit
val shutdown: T -> unit
@@ -21,13 +21,14 @@
datatype message = Message of string list;
-fun chunk s = [string_of_int (size s), "\n", s];
+fun chunk ss =
+ string_of_int (fold (Integer.add o size) ss 0) :: "\n" :: ss;
fun message name raw_props body =
let
val robust_props = map (pairself YXML.embed_controls) raw_props;
val header = YXML.string_of (XML.Elem ((name, robust_props), []));
- in Message (chunk header @ chunk body) end;
+ in Message (chunk [header] @ chunk body) end;
fun output_message channel (Message ss) =
List.app (System_Channel.output channel) ss;
@@ -37,7 +38,7 @@
fun flush channel = ignore (try System_Channel.flush channel);
-val flush_message = message Markup.protocolN Markup.flush "";
+val flush_message = message Markup.protocolN Markup.flush [];
fun flush_output channel = (output_message channel flush_message; flush channel);
--- a/src/Pure/Thy/thy_info.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Mar 31 21:15:26 2014 +0200
@@ -269,7 +269,7 @@
let
val _ = kill_thy name;
val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
- val _ = Output.try_protocol_message (Markup.loading_theory name) "";
+ val _ = Output.try_protocol_message (Markup.loading_theory name) [];
val {master = (thy_path, _), imports} = deps;
val dir = Path.dir thy_path;
--- a/src/Pure/Thy/thy_output.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon Mar 31 21:15:26 2014 +0200
@@ -109,7 +109,7 @@
in
[Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
- |> Pretty.chunks |> Pretty.writeln
+ |> Pretty.writeln_chunks
end;
fun antiquotation name scan body =
--- a/src/Pure/Thy/thy_syntax.scala Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon Mar 31 21:15:26 2014 +0200
@@ -262,14 +262,14 @@
syntax: Outer_Syntax,
node_name: Document.Node.Name,
span: List[Token],
- doc_blobs: Document.Blobs)
+ get_blob: Document.Node.Name => Option[Document.Blob])
: List[Command.Blob] =
{
span_files(syntax, span).map(file_name =>
Exn.capture {
val name =
Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
- val blob = doc_blobs.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
+ val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
(name, blob)
})
}
@@ -292,7 +292,7 @@
private def reparse_spans(
resources: Resources,
syntax: Outer_Syntax,
- doc_blobs: Document.Blobs,
+ get_blob: Document.Node.Name => Option[Document.Blob],
name: Document.Node.Name,
commands: Linear_Set[Command],
first: Command, last: Command): Linear_Set[Command] =
@@ -300,7 +300,7 @@
val cmds0 = commands.iterator(first, last).toList
val blobs_spans0 =
parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
- map(span => (resolve_files(resources, syntax, name, span, doc_blobs), span))
+ map(span => (resolve_files(resources, syntax, name, span, get_blob), span))
val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
@@ -327,7 +327,7 @@
private def recover_spans(
resources: Resources,
syntax: Outer_Syntax,
- doc_blobs: Document.Blobs,
+ get_blob: Document.Node.Name => Option[Document.Blob],
name: Document.Node.Name,
perspective: Command.Perspective,
commands: Linear_Set[Command]): Linear_Set[Command] =
@@ -343,7 +343,7 @@
case Some(first_unparsed) =>
val first = next_invisible_command(cmds.reverse, first_unparsed)
val last = next_invisible_command(cmds, first_unparsed)
- recover(reparse_spans(resources, syntax, doc_blobs, name, cmds, first, last))
+ recover(reparse_spans(resources, syntax, get_blob, name, cmds, first, last))
case None => cmds
}
recover(commands)
@@ -355,7 +355,7 @@
private def consolidate_spans(
resources: Resources,
syntax: Outer_Syntax,
- doc_blobs: Document.Blobs,
+ get_blob: Document.Node.Name => Option[Document.Blob],
reparse_limit: Int,
name: Document.Node.Name,
perspective: Command.Perspective,
@@ -375,7 +375,7 @@
last = it.next
i += last.length
}
- reparse_spans(resources, syntax, doc_blobs, name, commands, first_unfinished, last)
+ reparse_spans(resources, syntax, get_blob, name, commands, first_unfinished, last)
case None => commands
}
case None => commands
@@ -399,24 +399,24 @@
private def text_edit(
resources: Resources,
syntax: Outer_Syntax,
- doc_blobs: Document.Blobs,
+ get_blob: Document.Node.Name => Option[Document.Blob],
reparse_limit: Int,
node: Document.Node, edit: Document.Edit_Text): Document.Node =
{
edit match {
case (_, Document.Node.Clear()) => node.clear
- case (_, Document.Node.Blob()) => node.init_blob
+ case (_, Document.Node.Blob(blob)) => node.init_blob(blob)
case (name, Document.Node.Edits(text_edits)) =>
- if (node.is_blob) node
- else {
+ if (name.is_theory) {
val commands0 = node.commands
val commands1 = edit_text(text_edits, commands0)
val commands2 =
- recover_spans(resources, syntax, doc_blobs, name, node.perspective.visible, commands1)
+ recover_spans(resources, syntax, get_blob, name, node.perspective.visible, commands1)
node.update_commands(commands2)
}
+ else node
case (_, Document.Node.Deps(_)) => node
@@ -427,7 +427,7 @@
if (node.same_perspective(perspective)) node
else
node.update_perspective(perspective).update_commands(
- consolidate_spans(resources, syntax, doc_blobs, reparse_limit,
+ consolidate_spans(resources, syntax, get_blob, reparse_limit,
name, visible, node.commands))
}
}
@@ -439,6 +439,9 @@
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text]): Session.Change =
{
+ def get_blob(name: Document.Node.Name) =
+ doc_blobs.get(name) orElse previous.nodes(name).get_blob
+
val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
header_edits(resources.base_syntax, previous, edits)
@@ -469,11 +472,11 @@
val node1 =
if (reparse_set(name) && !commands.isEmpty)
node.update_commands(
- reparse_spans(resources, syntax, doc_blobs,
+ reparse_spans(resources, syntax, get_blob,
name, commands, commands.head, commands.last))
else node
val node2 =
- (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
+ (node1 /: edits)(text_edit(resources, syntax, get_blob, reparse_limit, _, _))
if (!(node.same_perspective(node2.perspective)))
doc_edits += (name -> node2.perspective)
--- a/src/Pure/Tools/proof_general.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Tools/proof_general.ML Mon Mar 31 21:15:26 2014 +0200
@@ -258,8 +258,8 @@
(* hooks *)
-fun message bg en prfx text =
- (case render text of
+fun message bg en prfx body =
+ (case render (implode body) of
"" => ()
| s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
@@ -276,7 +276,7 @@
(* notification *)
-val emacs_notify = message (special "I") (special "J") "";
+fun emacs_notify s = message (special "I") (special "J") "" [s];
fun tell_clear_goals () =
emacs_notify "Proof General, please clear the goals buffer.";
--- a/src/Pure/Tools/simplifier_trace.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML Mon Mar 31 21:15:26 2014 +0200
@@ -133,7 +133,7 @@
(** markup **)
fun output_result (id, data) =
- Output.result (Markup.serial_properties id) data
+ Output.result (Markup.serial_properties id) [data]
val parentN = "parent"
val textN = "text"
@@ -184,7 +184,7 @@
fun send_request (result_id, content) =
let
fun break () =
- (Output.protocol_message (Markup.simp_trace_cancel result_id) "";
+ (Output.protocol_message (Markup.simp_trace_cancel result_id) [];
Synchronized.change futures (Inttab.delete_safe result_id))
val promise = Future.promise break : string future
in
--- a/src/Pure/context_position.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/context_position.ML Mon Mar 31 21:15:26 2014 +0200
@@ -49,13 +49,13 @@
fun report_generic context pos markup =
if is_reported_generic context pos then
- Output.report (Position.reported_text pos markup "")
+ Output.report [Position.reported_text pos markup ""]
else ();
fun reported_text ctxt pos markup txt =
if is_reported ctxt pos then Position.reported_text pos markup txt else "";
-fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
+fun report_text ctxt pos markup txt = Output.report [reported_text ctxt pos markup txt];
fun report ctxt pos markup = report_text ctxt pos markup "";
fun reports_text ctxt reps = if is_visible ctxt then Position.reports_text reps else ();
--- a/src/Pure/skip_proof.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Pure/skip_proof.ML Mon Mar 31 21:15:26 2014 +0200
@@ -19,7 +19,7 @@
fun report ctxt =
if Context_Position.is_visible ctxt then
- Output.report (Markup.markup Markup.bad "Skipped proof")
+ Output.report [Markup.markup Markup.bad "Skipped proof"]
else ();
--- a/src/Tools/Code/code_preproc.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Tools/Code/code_preproc.ML Mon Mar 31 21:15:26 2014 +0200
@@ -181,7 +181,7 @@
val post = (#post o the_thmproc) thy;
val functrans = (map fst o #functrans o the_thmproc) thy;
in
- (Pretty.writeln o Pretty.chunks) [
+ Pretty.writeln_chunks [
Pretty.block [
Pretty.str "preprocessing simpset:",
Pretty.fbrk,
--- a/src/Tools/induct.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Tools/induct.ML Mon Mar 31 21:15:26 2014 +0200
@@ -254,7 +254,7 @@
pretty_rules ctxt "induct pred:" inductP,
pretty_rules ctxt "cases type:" casesT,
pretty_rules ctxt "cases pred:" casesP]
- |> Pretty.chunks |> Pretty.writeln
+ |> Pretty.writeln_chunks
end;
val _ =
--- a/src/Tools/jEdit/src/document_model.scala Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Mon Mar 31 21:15:26 2014 +0200
@@ -164,28 +164,25 @@
/* edits */
def node_edits(
- clear: Boolean,
- text_edits: List[Text.Edit],
- perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
- {
- Swing_Thread.require()
-
- if (is_theory) {
- val header_edit = session.header_edit(node_name, node_header())
- if (clear)
- List(header_edit,
- node_name -> Document.Node.Clear(),
- node_name -> Document.Node.Edits(text_edits),
- node_name -> perspective)
- else
- List(header_edit,
- node_name -> Document.Node.Edits(text_edits),
- node_name -> perspective)
+ clear: Boolean,
+ text_edits: List[Text.Edit],
+ perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
+ get_blob() match {
+ case None =>
+ val header_edit = session.header_edit(node_name, node_header())
+ if (clear)
+ List(header_edit,
+ node_name -> Document.Node.Clear(),
+ node_name -> Document.Node.Edits(text_edits),
+ node_name -> perspective)
+ else
+ List(header_edit,
+ node_name -> Document.Node.Edits(text_edits),
+ node_name -> perspective)
+ case Some(blob) =>
+ List(node_name -> Document.Node.Blob(blob),
+ node_name -> Document.Node.Edits(text_edits))
}
- else
- List(node_name -> Document.Node.Blob(),
- node_name -> Document.Node.Edits(text_edits))
- }
/* pending edits */
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Mon Mar 31 21:15:26 2014 +0200
@@ -110,6 +110,22 @@
/* dismiss */
+ private lazy val focus_delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
+ {
+ dismiss_unfocused()
+ }
+
+ def dismiss_unfocused()
+ {
+ stack.span(tip => !tip.pretty_text_area.isFocusOwner) match {
+ case (Nil, _) =>
+ case (unfocused, rest) =>
+ deactivate()
+ unfocused.foreach(_.hide_popup)
+ stack = rest
+ }
+ }
+
def dismiss(tip: Pretty_Tooltip)
{
deactivate()
@@ -189,13 +205,12 @@
override def focusGained(e: FocusEvent)
{
tip_border(true)
+ Pretty_Tooltip.focus_delay.invoke()
}
override def focusLost(e: FocusEvent)
{
- Pretty_Tooltip.hierarchy(tip) match {
- case Some((Nil, _)) => Pretty_Tooltip.dismiss(tip)
- case _ => tip_border(false)
- }
+ tip_border(false)
+ Pretty_Tooltip.focus_delay.invoke()
}
})
--- a/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 31 21:15:26 2014 +0200
@@ -122,7 +122,7 @@
if (new_text_info.isDefined)
text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get))
else
- text_area.getPainter.resetCursor
+ text_area.getPainter.setCursor(Cursor.getPredefinedCursor(Cursor.TEXT_CURSOR))
}
for {
r0 <- JEdit_Lib.visible_range(text_area)
@@ -590,6 +590,7 @@
def deactivate()
{
+ active_reset()
val painter = text_area.getPainter
view.removeWindowListener(window_listener)
text_area.removeFocusListener(focus_listener)
--- a/src/Tools/subtyping.ML Mon Mar 31 17:17:37 2014 +0200
+++ b/src/Tools/subtyping.ML Mon Mar 31 21:15:26 2014 +0200
@@ -1085,7 +1085,7 @@
[Pretty.big_list "coercions between base types:" (map show_coercion simple),
Pretty.big_list "other coercions:" (map show_coercion complex),
Pretty.big_list "coercion maps:" (map show_map tmaps)]
- end |> Pretty.chunks |> Pretty.writeln;
+ end |> Pretty.writeln_chunks;
(* theory setup *)