# HG changeset patch
# User wenzelm
# Date 1396293326 -7200
# Node ID 97d6a786e0f9c6299a20dcced580190903f18a54
# Parent  289dd9166d04b9d794a5b245aa17f6be1f0d18a3# Parent  075397022503c83ddd78160541e0f6e9b866eac9
merged

diff -r 289dd9166d04 -r 97d6a786e0f9 NEWS
--- 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.
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/HOL/SPARK/Tools/spark_commands.ML
--- 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 _ =
diff -r 289dd9166d04 -r 97d6a786e0f9 src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- 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
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- 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;
diff -r 289dd9166d04 -r 97d6a786e0f9 src/HOL/Tools/inductive.ML
--- 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 *)
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Provers/classical.ML
--- 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;
 
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Concurrent/future.ML
--- 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
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/General/output.ML
--- 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;
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/General/position.ML
--- 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;
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/General/pretty.ML
--- 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 **)
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/General/symbol.scala
--- 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
+      }
   }
 
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/General/timing.ML
--- 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
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/args.ML
--- 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;
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/attrib.ML
--- 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;
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/bundle.ML
--- 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;
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/calculation.ML
--- 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 *)
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/class.ML
--- 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;
 
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/code.ML
--- 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
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/context_rules.ML
--- 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 *)
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/isar_cmd.ML
--- 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);
 
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/isar_syn.ML
--- 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"
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/method.ML
--- 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
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/outer_syntax.ML
--- 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;
 
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/proof_context.ML
--- 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;
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Isar/toplevel.ML
--- 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
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/ML/ml_compiler_polyml.ML
--- 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
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/PIDE/command.ML
--- 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;
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/PIDE/command.scala
--- 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 + ")"
   }
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/PIDE/document.scala
--- 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(", ",", ")")
   }
 
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/PIDE/execution.ML
--- 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);
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/PIDE/protocol.ML
--- 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 _ =
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/PIDE/protocol.scala
--- 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 */
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/PIDE/query_operation.ML
--- 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 =
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/PIDE/resources.ML
--- 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;
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/PIDE/session.ML
--- 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;
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/PIDE/session.scala
--- 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)
           }
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Syntax/syntax.ML
--- 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;
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Syntax/syntax_phases.ML
--- 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;
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/System/invoke_scala.ML
--- 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);
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/System/isabelle_process.ML
--- 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;
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/System/message_channel.ML
--- 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);
 
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Thy/thy_info.ML
--- 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;
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Thy/thy_output.ML
--- 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 =
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Thy/thy_syntax.scala
--- 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)
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Tools/proof_general.ML
--- 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.";
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/Tools/simplifier_trace.ML
--- 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
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/context_position.ML
--- 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 ();
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Pure/skip_proof.ML
--- 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 ();
 
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Tools/Code/code_preproc.ML
--- 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,
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Tools/induct.ML
--- 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 _ =
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Tools/jEdit/src/document_model.scala
--- 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 */
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Tools/jEdit/src/pretty_tooltip.scala
--- 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()
     }
   })
 
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Tools/jEdit/src/rich_text_area.scala
--- 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)
diff -r 289dd9166d04 -r 97d6a786e0f9 src/Tools/subtyping.ML
--- 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 *)