# HG changeset patch
# User haftmann
# Date 1283346083 -7200
# Node ID e109feb514a8c4cb8e207ee77a8f1e3c0e780bc5
# Parent  10381eb983c1d4842e8904240947c73091557b93# Parent  cedf2ac63d9cb9d5917735dbd9235e3b20e63dd9
merged

diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/General/markup.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -14,8 +14,8 @@
   val properties: Properties.T -> T -> T
   val nameN: string
   val name: string -> T -> T
+  val kindN: string
   val bindingN: string val binding: string -> T
-  val kindN: string
   val entityN: string val entity: string -> T
   val defN: string
   val refN: string
@@ -115,8 +115,10 @@
   val assignN: string val assign: int -> T
   val editN: string val edit: int -> int -> T
   val pidN: string
+  val serialN: string
   val promptN: string val prompt: T
   val readyN: string val ready: T
+  val reportN: string val report: T
   val no_output: output * output
   val default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
@@ -163,13 +165,12 @@
 val nameN = "name";
 fun name a = properties [(nameN, a)];
 
-val (bindingN, binding) = markup_string "binding" nameN;
-
 val kindN = "kind";
 
 
 (* formal entities *)
 
+val (bindingN, binding) = markup_string "binding" nameN;
 val (entityN, entity) = markup_string "entity" nameN;
 
 val defN = "def";
@@ -337,10 +338,13 @@
 (* messages *)
 
 val pidN = "pid";
+val serialN = "serial";
 
 val (promptN, prompt) = markup_elem "prompt";
 val (readyN, ready) = markup_elem "ready";
 
+val (reportN, report) = markup_elem "report";
+
 
 
 (** print mode operations **)
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/General/markup.scala	Wed Sep 01 15:01:23 2010 +0200
@@ -69,6 +69,7 @@
 
   /* formal entities */
 
+  val BINDING = "binding"
   val ENTITY = "entity"
   val DEF = "def"
   val REF = "ref"
@@ -226,6 +227,7 @@
   /* messages */
 
   val PID = "pid"
+  val Serial = new Long_Property("serial")
 
   val MESSAGE = "message"
   val CLASS = "class"
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/General/position.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -27,6 +27,7 @@
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.T
+  val report_markup: T -> Markup.T
   val report_text: Markup.T -> T -> string -> unit
   val report: Markup.T -> T -> unit
   val str_of: T -> string
@@ -125,6 +126,8 @@
   if exists (member (op =) Markup.position_properties o #1) props then props
   else properties_of default @ props;
 
+fun report_markup pos = Markup.properties (properties_of pos) Markup.report;
+
 fun report_text markup (pos as Pos (count, _)) txt =
   if invalid_count count then ()
   else Output.report (Markup.markup (Markup.properties (properties_of pos) markup) txt);
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/General/position.scala	Wed Sep 01 15:01:23 2010 +0200
@@ -28,4 +28,15 @@
         case _ => None
       }
   }
+
+  object Id_Range
+  {
+    def unapply(pos: T): Option[(Long, Text.Range)] =
+      (pos, pos) match {
+        case (Id(id), Range(range)) => Some((id, range))
+        case _ => None
+      }
+  }
+
+  def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
 }
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/General/scan.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -105,7 +105,7 @@
 
 fun catch scan xs = scan xs
   handle ABORT msg => raise Fail msg
-    | FAIL msg => raise Fail (the_default "Syntax error." msg);
+    | FAIL msg => raise Fail (the_default "Syntax error" msg);
 
 
 (* scanner combinators *)
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/General/symbol.scala	Wed Sep 01 15:01:23 2010 +0200
@@ -53,6 +53,9 @@
 
   def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
 
+  def is_physical_newline(s: CharSequence): Boolean =
+    "\n".contentEquals(s) || "\r".contentEquals(s) || "\r\n".contentEquals(s)
+
   def is_wellformed(s: CharSequence): Boolean =
     s.length == 1 && is_plain(s.charAt(0)) || !bad_symbol.pattern.matcher(s).matches
 
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/General/xml.scala	Wed Sep 01 15:01:23 2010 +0200
@@ -102,17 +102,19 @@
         x
       }
 
+      def trim_bytes(s: String): String = new String(s.toCharArray)
+
       def cache_string(x: String): String =
         lookup(x) match {
           case Some(y) => y
-          case None => store(new String(x.toCharArray))  // trim string value
+          case None => store(trim_bytes(x))
         }
       def cache_props(x: List[(String, String)]): List[(String, String)] =
         if (x.isEmpty) x
         else
           lookup(x) match {
             case Some(y) => y
-            case None => store(x.map(p => (cache_string(p._1).intern, cache_string(p._2))))
+            case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
           }
       def cache_markup(x: Markup): Markup =
         lookup(x) match {
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -126,8 +126,8 @@
                 else error ("Type inference imposes additional sort constraint "
                   ^ Syntax.string_of_sort_global thy inferred_sort
                   ^ " of type parameter " ^ Name.aT ^ " of sort "
-                  ^ Syntax.string_of_sort_global thy a_sort ^ ".")
-            | _ => error "Multiple type variables in class specification.";
+                  ^ Syntax.string_of_sort_global thy a_sort)
+            | _ => error "Multiple type variables in class specification";
       in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
     val after_infer_fixate = (map o map_atyps)
       (fn T as TFree _ => T | T as TVar (vi, sort) =>
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -44,7 +44,6 @@
   val pwd: Toplevel.transition -> Toplevel.transition
   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
-  val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
   val print_context: Toplevel.transition -> Toplevel.transition
   val print_theory: bool -> Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
@@ -321,11 +320,6 @@
   in File.isabelle_tool "print" ("-c " ^ outfile); () end);
 
 
-(* pretty_setmargin *)
-
-fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.margin_default := n);
-
-
 (* print parts of theory and proof context *)
 
 val print_context = Toplevel.keep Toplevel.print_state_context;
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -786,7 +786,8 @@
 
 val _ =
   Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
-    Keyword.diag (Parse.nat >> (Toplevel.no_timing oo Isar_Cmd.pretty_setmargin));
+    Keyword.diag (Parse.nat >>
+      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
 
 val _ =
   Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag
@@ -991,7 +992,7 @@
     (Scan.succeed
       (Toplevel.no_timing o Toplevel.keep (fn state =>
         (Context.set_thread_data (try Toplevel.generic_theory_of state);
-          raise Toplevel.TERMINATE))));
+          raise Runtime.TERMINATE))));
 
 end;
 
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -181,7 +181,7 @@
       if Thm.concl_of th aconv thesis andalso
         Logic.strip_assums_concl prem aconv thesis then th
       else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
-  | [] => error "Goal solved -- nothing guessed."
+  | [] => error "Goal solved -- nothing guessed"
   | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
 
 fun result tac facts ctxt =
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/Isar/runtime.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -11,6 +11,7 @@
   exception EXCURSION_FAIL of exn * string
   exception TOPLEVEL_ERROR
   val exn_context: Proof.context option -> exn -> exn
+  val exn_messages: (exn -> Position.T) -> exn -> string list
   val exn_message: (exn -> Position.T) -> exn -> string
   val debugging: ('a -> 'b) -> 'a -> 'b
   val controlled_execution: ('a -> 'b) -> 'a -> 'b
@@ -41,7 +42,7 @@
 fun if_context NONE _ _ = []
   | if_context (SOME ctxt) f xs = map (f ctxt) xs;
 
-fun exn_message exn_position e =
+fun exn_messages exn_position e =
   let
     fun raised exn name msgs =
       let val pos = Position.str_of (exn_position exn) in
@@ -53,32 +54,36 @@
 
     val detailed = ! Output.debugging;
 
-    fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
-      | exn_msg _ (Exn.EXCEPTIONS []) = "Exception."
-      | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
-      | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
-          exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
-      | exn_msg _ TERMINATE = "Exit."
-      | exn_msg _ Exn.Interrupt = "Interrupt."
-      | exn_msg _ TimeLimit.TimeOut = "Timeout."
-      | exn_msg _ TOPLEVEL_ERROR = "Error."
-      | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
-      | exn_msg _ (ERROR msg) = msg
-      | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
-      | exn_msg _ (exn as THEORY (msg, thys)) =
-          raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
-      | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
-            (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
-      | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
+    fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn
+      | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
+      | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
+          map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
+      | exn_msgs _ TERMINATE = ["Exit"]
+      | exn_msgs _ Exn.Interrupt = []
+      | exn_msgs _ TimeLimit.TimeOut = ["Timeout"]
+      | exn_msgs _ TOPLEVEL_ERROR = ["Error"]
+      | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
+      | exn_msgs _ (ERROR msg) = [msg]
+      | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
+      | exn_msgs _ (exn as THEORY (msg, thys)) =
+          [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
+      | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg ::
+            (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
+      | exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg ::
             (if detailed then
               if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
-             else []))
-      | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
-            (if detailed then if_context ctxt Syntax.string_of_term ts else []))
-      | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
-            (if detailed then if_context ctxt Display.string_of_thm thms else []))
-      | exn_msg _ exn = raised exn (General.exnMessage exn) [];
-  in exn_msg NONE e end;
+             else []))]
+      | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg ::
+            (if detailed then if_context ctxt Syntax.string_of_term ts else []))]
+      | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg ::
+            (if detailed then if_context ctxt Display.string_of_thm thms else []))]
+      | exn_msgs _ exn = [raised exn (General.exnMessage exn) []];
+  in exn_msgs NONE e end;
+
+fun exn_message exn_position exn =
+  (case exn_messages exn_position exn of
+    [] => "Interrupt"
+  | msgs => cat_lines msgs);
 
 
 
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -30,19 +30,20 @@
   val timing: bool Unsynchronized.ref
   val profiling: int Unsynchronized.ref
   val skip_proofs: bool Unsynchronized.ref
-  exception TERMINATE
   exception TOPLEVEL_ERROR
   val program: (unit -> 'a) -> 'a
   val thread: bool -> (unit -> unit) -> Thread.thread
   type transition
   val empty: transition
   val init_of: transition -> string option
+  val print_of: transition -> bool
   val name_of: transition -> string
   val pos_of: transition -> Position.T
   val str_of: transition -> string
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
   val interactive: bool -> transition -> transition
+  val set_print: bool -> transition -> transition
   val print: transition -> transition
   val no_timing: transition -> transition
   val init_theory: string -> (unit -> theory) -> transition -> transition
@@ -84,10 +85,9 @@
   val unknown_context: transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val status: transition -> Markup.T -> unit
-  val error_msg: transition -> exn * string -> unit
+  val error_msg: transition -> string -> unit
   val add_hook: (transition -> state -> state -> unit) -> unit
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
-  val run_command: string -> transition -> state -> state option
   val command: transition -> state -> state
   val excursion: (transition * transition list) list -> (transition * state) list lazy * theory
 end;
@@ -222,8 +222,6 @@
 val profiling = Unsynchronized.ref 0;
 val skip_proofs = Unsynchronized.ref false;
 
-exception TERMINATE = Runtime.TERMINATE;
-exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
 exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
 
 fun program body =
@@ -351,12 +349,13 @@
 fun init_of (Transition {trans = [Init (name, _)], ...}) = SOME name
   | init_of _ = NONE;
 
+fun print_of (Transition {print, ...}) = print;
 fun name_of (Transition {name, ...}) = name;
 fun pos_of (Transition {pos, ...}) = pos;
 fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr);
 
 fun command_msg msg tr = msg ^ "command " ^ str_of tr;
-fun at_command tr = command_msg "At " tr ^ ".";
+fun at_command tr = command_msg "At " tr;
 
 fun type_error tr state =
   ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
@@ -563,9 +562,8 @@
 fun status tr m =
   setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
 
-fun error_msg tr exn_info =
-  setmp_thread_position tr (fn () =>
-    Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
+fun error_msg tr msg =
+  setmp_thread_position tr (fn () => Output.error_msg msg) ();
 
 
 (* post-transition hooks *)
@@ -609,8 +607,8 @@
     val ctxt = try context_of st;
     val res =
       (case app int tr st of
-        (_, SOME TERMINATE) => NONE
-      | (st', SOME (EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
+        (_, SOME Runtime.TERMINATE) => NONE
+      | (st', SOME (Runtime.EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
       | (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr))
       | (st', NONE) => SOME (st', NONE));
     val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
@@ -619,53 +617,13 @@
 end;
 
 
-(* managed execution *)
-
-local
-
-fun async_state (tr as Transition {print, ...}) st =
-  if print then
-    ignore
-      (Future.fork (fn () =>
-          setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
-  else ();
-
-fun proof_status tr st =
-  (case try proof_of st of
-    SOME prf => status tr (Proof.status_markup prf)
-  | NONE => ());
-
-in
-
-fun run_command thy_name tr st =
-  (case
-      (case init_of tr of
-        SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
-      | NONE => Exn.Result ()) of
-    Exn.Result () =>
-      let val int = is_some (init_of tr) in
-        (case transition int tr st of
-          SOME (st', NONE) =>
-           (status tr Markup.finished;
-            proof_status tr st';
-            if int then () else async_state tr st';
-            SOME st')
-        | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
-        | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
-        | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
-      end
-  | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
-
-end;
-
-
 (* nested commands *)
 
 fun command tr st =
   (case transition (! interact) tr st of
     SOME (st', NONE) => st'
-  | SOME (_, SOME exn_info) => raise EXCURSION_FAIL exn_info
-  | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
+  | SOME (_, SOME exn_info) => raise Runtime.EXCURSION_FAIL exn_info
+  | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
 
 fun command_result tr st =
   let val st' = command tr st
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -7,6 +7,7 @@
 signature ML_COMPILER =
 sig
   val exn_position: exn -> Position.T
+  val exn_messages: exn -> string list
   val exn_message: exn -> string
   val eval: bool -> Position.T -> ML_Lex.token list -> unit
 end
@@ -15,6 +16,7 @@
 struct
 
 fun exn_position _ = Position.none;
+val exn_messages = Runtime.exn_messages exn_position;
 val exn_message = Runtime.exn_message exn_position;
 
 fun eval verbose pos toks =
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -4,13 +4,6 @@
 Advanced runtime compilation for Poly/ML 5.3.0.
 *)
 
-signature ML_COMPILER =
-sig
-  val exn_position: exn -> Position.T
-  val exn_message: exn -> string
-  val eval: bool -> Position.T -> ML_Lex.token list -> unit
-end
-
 structure ML_Compiler: ML_COMPILER =
 struct
 
@@ -37,6 +30,7 @@
     NONE => Position.none
   | SOME loc => position_of loc);
 
+val exn_messages = Runtime.exn_messages exn_position;
 val exn_message = Runtime.exn_message exn_position;
 
 
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Sep 01 15:01:23 2010 +0200
@@ -8,23 +8,25 @@
 package isabelle
 
 
+import scala.collection.immutable.SortedMap
+
+
 object Command
 {
   /** accumulated results from prover **/
 
   case class State(
     val command: Command,
-    val status: List[Markup],
-    val reverse_results: List[XML.Tree],
-    val markup: Markup_Tree)
+    val status: List[Markup] = Nil,
+    val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
+    val markup: Markup_Tree = Markup_Tree.empty)
   {
     /* content */
 
-    lazy val results = reverse_results.reverse
-
     def add_status(st: Markup): State = copy(status = st :: status)
     def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
-    def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
+    def add_result(serial: Long, result: XML.Tree): State =
+      copy(results = results + (serial -> result))
 
     def root_info: Text.Info[Any] =
       new Text.Info(command.range,
@@ -34,7 +36,7 @@
 
     /* message dispatch */
 
-    def accumulate(message: XML.Tree): Command.State =
+    def accumulate(message: XML.Elem): Command.State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>
@@ -46,15 +48,22 @@
         case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
           (this /: msgs)((state, msg) =>
             msg match {
-              case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
-              if Position.Id.unapply(atts) == Some(command.id) =>
-                val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
+              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args)
+              if id == command.id =>
+                val props = Position.purge(atts)
                 val info =
                   Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
                 state.add_markup(info)
               case _ => System.err.println("Ignored report message: " + msg); state
             })
-        case _ => add_result(message)
+        case XML.Elem(Markup(name, atts), body) =>
+          atts match {
+            case Markup.Serial(i) =>
+              val result = XML.Elem(Markup(name, Position.purge(atts)), body)
+              (add_result(i, result) /: Isar_Document.reported_positions(command.id, message))(
+                (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
+            case _ => System.err.println("Ignored message without serial number: " + message); this
+          }
       }
   }
 
@@ -89,6 +98,10 @@
   def source(range: Text.Range): String = source.substring(range.start, range.stop)
   def length: Int = source.length
 
+  val newlines =
+    (0 /: Symbol.iterator(source)) {
+      case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n }
+
   val range: Text.Range = Text.Range(0, length)
 
   lazy val symbol_index = new Symbol.Index(source)
@@ -98,5 +111,5 @@
 
   /* accumulated results */
 
-  val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
+  val empty_state: Command.State = Command.State(this)
 }
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -192,6 +192,59 @@
 
 
 
+(* toplevel transactions *)
+
+local
+
+fun proof_status tr st =
+  (case try Toplevel.proof_of st of
+    SOME prf => Toplevel.status tr (Proof.status_markup prf)
+  | NONE => ());
+
+fun async_state tr st =
+  if Toplevel.print_of tr then
+    ignore
+      (Future.fork
+        (fn () =>
+          Toplevel.setmp_thread_position tr
+            (fn () => Future.status (fn () => Toplevel.print_state false st)) ()))
+  else ();
+
+in
+
+fun run_command thy_name tr st =
+  (case
+      (case Toplevel.init_of tr of
+        SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
+      | NONE => Exn.Result ()) of
+    Exn.Result () =>
+      let
+        val int = is_some (Toplevel.init_of tr);
+        val (errs, result) =
+          (case Toplevel.transition int tr st of
+            SOME (st', NONE) => ([], SOME st')
+          | SOME (_, SOME exn_info) =>
+              (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
+                [] => raise Exn.Interrupt
+              | errs => (errs, NONE))
+          | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
+        val _ = List.app (Toplevel.error_msg tr) errs;
+        val _ =
+          (case result of
+            NONE => Toplevel.status tr Markup.failed
+          | SOME st' =>
+             (Toplevel.status tr Markup.finished;
+              proof_status tr st';
+              if int then () else async_state tr st'));
+      in result end
+  | Exn.Exn exn =>
+     (Toplevel.error_msg tr (ML_Compiler.exn_message exn); Toplevel.status tr Markup.failed; NONE))
+
+end;
+
+
+
+
 (** editing **)
 
 (* edit *)
@@ -214,7 +267,7 @@
           NONE => NONE
         | SOME st =>
             let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
-            in Toplevel.run_command name exec_tr st end));
+            in run_command name exec_tr st end));
     val state' = define_exec exec_id' exec' state;
   in (exec_id', (id, exec_id') :: updates, state') end;
 
@@ -263,7 +316,8 @@
         | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
 
       val _ = List.app Future.cancel execution;
-      fun await_cancellation () = uninterruptible (fn _ => Future.join_results) execution;
+      fun await_cancellation () =
+        uninterruptible (fn _ => fn () => Future.join_results execution) ();
 
       val execution' = (* FIXME proper node deps *)
         node_names_of version |> map (fn name =>
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Sep 01 15:01:23 2010 +0200
@@ -44,7 +44,6 @@
   {
     val empty: Node = new Node(Linear_Set())
 
-    // FIXME not scalable
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
     {
@@ -57,16 +56,36 @@
     }
   }
 
+  private val block_size = 1024
+
   class Node(val commands: Linear_Set[Command])
   {
-    def command_starts: Iterator[(Command, Text.Offset)] =
-      Node.command_starts(commands.iterator)
+    private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
+    {
+      val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
+      var next_block = 0
+      var last_stop = 0
+      for ((command, start) <- Node.command_starts(commands.iterator)) {
+        last_stop = start + command.length
+        while (last_stop + 1 > next_block) {
+          blocks += (command -> start)
+          next_block += block_size
+        }
+      }
+      (blocks.toArray, Text.Range(0, last_stop))
+    }
 
-    def command_start(cmd: Command): Option[Text.Offset] =
-      command_starts.find(_._1 == cmd).map(_._2)
+    def full_range: Text.Range = full_index._2
 
     def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
-      command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
+    {
+      if (!commands.isEmpty && full_range.contains(i)) {
+        val (cmd0, start0) = full_index._1(i / block_size)
+        Node.command_starts(commands.iterator(cmd0), start0) dropWhile {
+          case (cmd, start) => start + cmd.length <= i }
+      }
+      else Iterator.empty
+    }
 
     def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
       command_range(range.start) takeWhile { case (_, start) => start < range.stop }
@@ -83,6 +102,12 @@
           commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
         case None => None
       }
+
+    def command_start(cmd: Command): Option[Text.Offset] =
+      command_starts.find(_._1 == cmd).map(_._2)
+
+    def command_starts: Iterator[(Command, Text.Offset)] =
+      Node.command_starts(commands.iterator)
   }
 
 
@@ -155,7 +180,7 @@
   {
     class Fail(state: State) extends Exception
 
-    val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)
+    val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)._2
 
     class Assignment(former_assignment: Map[Command, Exec_ID])
     {
@@ -204,7 +229,7 @@
     def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
     def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
 
-    def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
+    def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
       execs.get(id) match {
         case Some((st, occs)) =>
           val new_st = st.accumulate(message)
@@ -218,7 +243,7 @@
           }
       }
 
-    def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
+    def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
     {
       val version = the_version(id)
       val occs = Set(version)  // FIXME unused (!?)
@@ -232,7 +257,7 @@
           (st.command, exec_id)
         }
       the_assignment(version).assign(assigned_execs)  // FIXME explicit value instead of promise (!?)
-      copy(execs = new_execs)
+      (assigned_execs.map(_._1), copy(execs = new_execs))
     }
 
     def is_assigned(version: Version): Boolean =
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Wed Sep 01 15:01:23 2010 +0200
@@ -54,6 +54,22 @@
     else if (markup.exists(_.name == Markup.FINISHED)) Finished
     else Unprocessed
   }
+
+
+  /* reported positions */
+
+  def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
+  {
+    def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
+      tree match {
+        case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
+        if (name == Markup.BINDING || name == Markup.ENTITY || name == Markup.REPORT) &&
+          id == command_id => body.foldLeft(set + range)(reported)
+        case XML.Elem(_, body) => body.foldLeft(set)(reported)
+        case XML.Text(_) => set
+      }
+    reported(Set.empty, message) ++ Position.Range.unapply(message.markup.properties)
+  }
 }
 
 
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/ROOT.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -179,9 +179,9 @@
 use "ML/ml_syntax.ML";
 use "ML/ml_env.ML";
 use "Isar/runtime.ML";
+use "ML/ml_compiler.ML";
 if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
-  String.isPrefix "smlnj" ml_system
-then use "ML/ml_compiler.ML"
+  String.isPrefix "smlnj" ml_system then ()
 else use "ML/ml_compiler_polyml-5.3.ML";
 use "ML/ml_context.ML";
 
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/Syntax/parser.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -773,7 +773,7 @@
                   if not (! warned) andalso
                      length (new_states @ States) > ! branching_level then
                     (Context_Position.if_visible ctxt warning
-                      "Currently parsed expression could be extremely ambiguous.";
+                      "Currently parsed expression could be extremely ambiguous";
                      warned := true)
                   else ();
               in
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -63,7 +63,8 @@
 in
 
 fun standard_message out_stream ch body =
-  message out_stream ch (Position.properties_of (Position.thread_data ())) body;
+  message out_stream ch
+    ((Markup.serialN, serial_string ()) :: Position.properties_of (Position.thread_data ())) body;
 
 fun init_message out_stream =
   message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/System/isar.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -94,7 +94,10 @@
 fun op >> tr =
   (case Toplevel.transition true tr (state ()) of
     NONE => false
-  | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
+  | SOME (_, SOME exn_info) =>
+     (set_exn (SOME exn_info);
+      Toplevel.error_msg tr (ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
+      true)
   | SOME (st', NONE) =>
       let
         val name = Toplevel.name_of tr;
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/System/session.scala	Wed Sep 01 15:01:23 2010 +0200
@@ -190,7 +190,8 @@
             result.body match {
               case List(Isar_Document.Assign(id, edits)) =>
                 try {
-                  global_state.change(_.assign(id, edits))
+                  val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
+                  for (cmd <- cmds) command_change_buffer ! cmd
                   assignments.event(Session.Assignment)
                 }
                 catch { case _: Document.State.Fail => bad_result(result) }
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Sep 01 15:01:23 2010 +0200
@@ -77,9 +77,11 @@
       commands.iterator.find(_.is_unparsed) match {
         case Some(first_unparsed) =>
           val first =
-            commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
+            commands.reverse_iterator(first_unparsed).
+              dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head
           val last =
-            commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
+            commands.iterator(first_unparsed).
+              dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
           val range =
             commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
 
diff -r cedf2ac63d9c -r e109feb514a8 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Pure/goal.ML	Wed Sep 01 15:01:23 2010 +0200
@@ -159,7 +159,7 @@
   (case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
     SOME th => Drule.implies_intr_list casms
       (finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
-  | NONE => error "Tactic failed.");
+  | NONE => error "Tactic failed");
 
 
 (* prove_common etc. *)
@@ -191,7 +191,7 @@
 
     fun result () =
       (case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of
-        NONE => err "Tactic failed."
+        NONE => err "Tactic failed"
       | SOME st =>
           let val res = finish ctxt' st handle THM (msg, _, _) => err msg in
             if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]
diff -r cedf2ac63d9c -r e109feb514a8 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Wed Sep 01 15:01:23 2010 +0200
@@ -190,19 +190,6 @@
 
 class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
 {
-  /* visible line end */
-
-  // simplify slightly odd result of TextArea.getLineEndOffset
-  // NB: jEdit already normalizes \r\n and \r to \n
-  def visible_line_end(start: Text.Offset, end: Text.Offset): Text.Offset =
-  {
-    val end1 = end - 1
-    if (start <= end1 && end1 < buffer.getLength &&
-        buffer.getSegment(end1, 1).charAt(0) == '\n') end1
-    else end
-  }
-
-
   /* pending text edits */
 
   object pending_edits  // owned by Swing thread
diff -r cedf2ac63d9c -r e109feb514a8 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Wed Sep 01 15:01:23 2010 +0200
@@ -97,6 +97,24 @@
   }
 
 
+  /* visible line ranges */
+
+  // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
+  // NB: jEdit already normalizes \r\n and \r to \n
+  def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
+  {
+    val stop = if (start < end) end - 1 else end min model.buffer.getLength
+    Text.Range(start, stop)
+  }
+
+  def screen_lines_range(): Text.Range =
+  {
+    val start = text_area.getScreenLineStartOffset(0)
+    val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
+    proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
+  }
+
+
   /* commands_changed_actor */
 
   private val commands_changed_actor = actor {
@@ -106,23 +124,25 @@
           val buffer = model.buffer
           Isabelle.swing_buffer_lock(buffer) {
             val snapshot = model.snapshot()
-            if (changed.exists(snapshot.node.commands.contains)) {
-              var visible_change = false
-              for ((command, start) <- snapshot.node.command_starts) {
-                if (changed(command)) {
-                  val stop = start + command.length
-                  val line1 = buffer.getLineOfOffset(snapshot.convert(start))
-                  val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
-                  if (line2 >= text_area.getFirstLine &&
-                      line1 <= text_area.getFirstLine + text_area.getVisibleLines)
-                    visible_change = true
-                  text_area.invalidateLineRange(line1, line2)
-                }
-              }
+
+            if (changed.exists(snapshot.node.commands.contains))
+              overview.repaint()
+
+            val visible_range = screen_lines_range()
+            val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
+            if (visible_cmds.exists(changed)) {
+              for {
+                line <- 0 until text_area.getVisibleLines
+                val start = text_area.getScreenLineStartOffset(line) if start >= 0
+                val end = text_area.getScreenLineEndOffset(line) if end >= 0
+                val range = proper_line_range(start, end)
+                val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+                if line_cmds.exists(changed)
+              } text_area.invalidateScreenLineRange(line, line)
+
               // FIXME danger of deadlock!?
-              if (visible_change) model.buffer.propertiesChanged()
-
-              overview.repaint()  // FIXME really paint here!?
+              // FIXME potentially slow!?
+              model.buffer.propertiesChanged()
             }
           }
 
@@ -138,49 +158,26 @@
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
-      start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
+      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       Isabelle.swing_buffer_lock(model.buffer) {
         val snapshot = model.snapshot()
-
-        val command_range: Iterable[(Command, Text.Offset)] =
-        {
-          val range = snapshot.node.command_range(snapshot.revert(start(0)))
-          if (range.hasNext) {
-            val (cmd0, start0) = range.next
-            new Iterable[(Command, Text.Offset)] {
-              def iterator =
-                Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
-            }
-          }
-          else Iterable.empty
-        }
-
         val saved_color = gfx.getColor
         try {
-          var y = y0
           for (i <- 0 until physical_lines.length) {
             if (physical_lines(i) != -1) {
-              val line_start = start(i)
-              val line_end = model.visible_line_end(line_start, end(i))
-
-              val a = snapshot.revert(line_start)
-              val b = snapshot.revert(line_end)
-              val cmds = command_range.iterator.
-                dropWhile { case (cmd, c) => c + cmd.length <= a } .
-                takeWhile { case (_, c) => c < b }
-
+              val line_range = proper_line_range(start(i), end(i))
+              val cmds = snapshot.node.command_range(snapshot.revert(line_range))
               for ((command, command_start) <- cmds if !command.is_ignored) {
-                val p =
-                  text_area.offsetToXY(line_start max snapshot.convert(command_start))
-                val q =
-                  text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
-                if (p.y != q.y) System.err.println("Unexpected coordinates: " + p + ", " + q)
-                gfx.setColor(Document_View.choose_color(snapshot, command))
-                gfx.fillRect(p.x, y, q.x - p.x, line_height)
+                val range = line_range.restrict(snapshot.convert(command.range + command_start))
+                val p = text_area.offsetToXY(range.start)
+                val q = text_area.offsetToXY(range.stop)
+                if (p != null && q != null) {
+                  gfx.setColor(Document_View.choose_color(snapshot, command))
+                  gfx.fillRect(p.x, y + i * line_height, q.x - p.x, line_height)
+                }
               }
             }
-            y += line_height
           }
         }
         finally { gfx.setColor(saved_color) }
diff -r cedf2ac63d9c -r e109feb514a8 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed Sep 01 15:01:13 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed Sep 01 15:01:23 2010 +0200
@@ -67,12 +67,12 @@
             case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
               val snapshot = doc_view.model.snapshot()
               val filtered_results =
-                snapshot.state(cmd).results filter {
+                snapshot.state(cmd).results.iterator.map(_._2) filter {
                   case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
                   case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
                   case _ => true
                 }
-              html_panel.render(filtered_results)
+              html_panel.render(filtered_results.toList)
             case _ =>
           }
         case None =>