simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
eliminated separate Outer_Syntax.read_element;

--- a/src/Pure/Isar/outer_syntax.ML	Sun Feb 24 14:14:07 2013 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sun Feb 24 17:29:55 2013 +0100
@@ -35,9 +35,7 @@
   type isar
   val isar: TextIO.instream -> bool -> isar
   val span_cmts: Token.T list -> Token.T list
-  val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
-  val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.span Thy_Syntax.element ->
-    (Toplevel.transition * Toplevel.transition list) list
+  val read_span: outer_syntax -> Token.T list -> Toplevel.transition
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -319,30 +317,16 @@
     val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
     val _ = Position.reports_text (token_reports @ maps command_reports toks);
   in
-    if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true)
+    if is_malformed then Toplevel.malformed pos "Malformed command syntax"
     else
       (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
         [tr] =>
           if Keyword.is_control (Toplevel.name_of tr) then
-            (Toplevel.malformed pos "Illegal control command", true)
-          else (tr, true)
-      | [] => (Toplevel.ignored (Position.set_range (Command.range toks)), false)
-      | _ => (Toplevel.malformed proper_range "Exactly one command expected", true))
-      handle ERROR msg => (Toplevel.malformed proper_range msg, true)
-  end;
-
-fun read_element outer_syntax init (Thy_Syntax.Element (head, opt_proof)) =
-  let
-    val read = read_span outer_syntax o Thy_Syntax.span_content;
-    val (tr, proper_head) = read head |>> Toplevel.modify_init init;
-    val proof_trs =
-      (case opt_proof of
-        NONE => []
-      | SOME (a, b) => map read (maps Thy_Syntax.flat_element a @ [b]) |> filter #2 |> map #1);
-  in
-    if proper_head andalso
-      not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
-    else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
+            Toplevel.malformed pos "Illegal control command"
+          else tr
+      | [] => Toplevel.ignored (Position.set_range (Command.range toks))
+      | _ => Toplevel.malformed proper_range "Exactly one command expected")
+      handle ERROR msg => Toplevel.malformed proper_range msg
   end;
 
 end;

--- a/src/Pure/Isar/toplevel.ML	Sun Feb 24 14:14:07 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sun Feb 24 17:29:55 2013 +0100
@@ -51,6 +51,7 @@
   val keep': (bool -> state -> unit) -> transition -> transition
   val imperative: (unit -> unit) -> transition -> transition
   val ignored: Position.T -> transition
+  val is_ignored: transition -> bool
   val malformed: Position.T -> string -> transition
   val is_malformed: transition -> bool
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
@@ -414,6 +415,7 @@
 fun imperative f = keep (fn _ => f ());
 
 fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
+fun is_ignored tr = name_of tr = "<ignored>";
 
 val malformed_name = "<malformed>";
 fun malformed pos msg =

--- a/src/Pure/PIDE/document.ML	Sun Feb 24 14:14:07 2013 +0100
+++ b/src/Pure/PIDE/document.ML	Sun Feb 24 17:29:55 2013 +0100
@@ -268,9 +268,8 @@
       val id_string = print_id id;
       val span = Lazy.lazy (fn () =>
         Position.setmp_thread_data (Position.id_only id_string)
-          (fn () =>
-            Thy_Syntax.parse_tokens
-              (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ());
+          (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
+            ());
       val _ =
         Position.setmp_thread_data (Position.id_only id_string)
           (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
@@ -453,7 +452,7 @@
           (fn () =>
             let
               val tr =
-                #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
+                Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
                 |> modify_init
                 |> Toplevel.put_id exec_id'_string;
               val cmts = Outer_Syntax.span_cmts span;

--- a/src/Pure/Thy/thy_load.ML	Sun Feb 24 14:14:07 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sun Feb 24 17:29:55 2013 +0100
@@ -218,18 +218,30 @@
   let
     val immediate = not (Goal.future_enabled ());
 
-    fun put_timing tr = Toplevel.put_timing (last_timing tr) tr;
-    fun put_timings (tr, trs) = (put_timing tr, map put_timing trs);
+    fun prepare_span span =
+      Thy_Syntax.span_content span
+      |> Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ()))
+      |> Toplevel.modify_init init
+      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
 
-    fun proof_result (tr, trs) (st, _) =
+    fun element_result span_elem (st, _) =
       let
-        val (result, st') = Toplevel.proof_result immediate (tr, trs) st;
-        val pos' = Toplevel.pos_of (List.last (tr :: trs));
-      in (result, (st', pos')) end;
+        val tr_elem = Thy_Syntax.map_element prepare_span span_elem;
+        val Thy_Syntax.Element (tr, opt_proof) = tr_elem;
+        val proof_trs =
+          (case opt_proof of
+            NONE => []
+          | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out Toplevel.is_ignored);
 
-    fun element_result elem x =
-      fold_map (proof_result o put_timings)
-        (Outer_Syntax.read_element (#2 (Outer_Syntax.get_syntax ())) init elem) x;
+        val elems =
+          if Toplevel.is_ignored tr then map (rpair []) proof_trs
+          else if Keyword.is_schematic_goal (Toplevel.name_of tr)
+          then map (rpair []) (tr :: proof_trs)
+          else [(tr, proof_trs)];
+
+        val (results, st') = fold_map (Toplevel.proof_result immediate) elems st;
+        val pos' = Toplevel.pos_of (Thy_Syntax.last_element tr_elem);
+      in (results, (st', pos')) end;
 
     val (results, (end_state, end_pos)) =
       fold_map element_result elements (Toplevel.toplevel, Position.none);

--- a/src/Pure/Thy/thy_syntax.ML	Sun Feb 24 14:14:07 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Sun Feb 24 17:29:55 2013 +0100
@@ -18,6 +18,7 @@
   datatype 'a element = Element of 'a * ('a element list * 'a) option
   val map_element: ('a -> 'b) -> 'a element -> 'b element
   val flat_element: 'a element -> 'a list
+  val last_element: 'a element -> 'a
   val parse_elements: span list -> span element list
 end;
 
@@ -148,6 +149,9 @@
 fun flat_element (Element (a, NONE)) = [a]
   | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
 
+fun last_element (Element (a, NONE)) = a
+  | last_element (Element (_, SOME (_, b))) = b;
+
 
 (* scanning spans *)