src/Pure/Isar/outer_syntax.ML

   val local_theory_to_proof': command_keyword -> string ->
     (bool -> local_theory -> Proof.state) parser -> unit
   val local_theory_to_proof: command_keyword -> string ->
     (local_theory -> Proof.state) parser -> unit
   val bootstrap: bool Config.T
-  val parse_tokens: theory -> Token.T list -> Toplevel.transition list
-  val parse: theory -> Position.T -> string -> Toplevel.transition list
   val parse_spans: Token.T list -> Command_Span.span list
   val make_span: Token.T list -> Command_Span.span
+  val parse_span: theory -> (unit -> theory) -> Token.T list -> Toplevel.transition
+  val parse_text: theory -> (unit -> theory) -> Position.T -> string -> Toplevel.transition list
   val command_reports: theory -> Token.T -> Position.report_text list
   val check_command: Proof.context -> command_keyword -> string
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =

 
 
 
 (** toplevel parsing **)
 
+(* parse spans *)
+
+local
+
+fun ship span =
+  let
+    val kind =
+      if forall Token.is_ignored span then Command_Span.Ignored_Span
+      else if exists Token.is_error span then Command_Span.Malformed_Span
+      else
+        (case find_first Token.is_command span of
+          NONE => Command_Span.Malformed_Span
+        | SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd));
+  in cons (Command_Span.Span (kind, span)) end;
+
+fun flush (result, content, ignored) =
+  result
+  |> not (null content) ? ship (rev content)
+  |> not (null ignored) ? ship (rev ignored);
+
+fun parse tok (result, content, ignored) =
+  if Token.is_ignored tok then (result, content, tok :: ignored)
+  else if Token.is_command_modifier tok orelse
+    Token.is_command tok andalso
+      (not (exists Token.is_command_modifier content) orelse exists Token.is_command content)
+  then (flush (result, content, ignored), [tok], [])
+  else (result, tok :: (ignored @ content), []);
+
+in
+
+fun parse_spans toks =
+  fold parse toks ([], [], []) |> flush |> rev;
+
+end;
+
+fun make_span toks =
+  (case parse_spans toks of
+    [span] => span
+  | _ => Command_Span.Span (Command_Span.Malformed_Span, toks));
+
+
 (* parse commands *)
 
 val bootstrap = Config.declare_bool ("Outer_Syntax.bootstrap", \<^here>) (K true);
 
 local
 
 val before_command =
   Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
 
-fun parse_command thy =
+fun parse_command thy markers =
   Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
     let
       val keywords = Thy_Header.get_keywords thy;
       val tr0 =
         Toplevel.empty
         |> Toplevel.name name
         |> Toplevel.position pos
         |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
         |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
-      val command_marker =
-        Parse.command |-- Document_Source.annotation >> (fn markers => Toplevel.markers markers tr0);
+      val command_markers =
+        Parse.command |-- Document_Source.tags >>
+          (fn tags => Toplevel.markers (map Document_Marker.legacy_tag tags @ markers) tr0);
     in
       (case lookup_commands thy name of
         SOME (Command {command_parser = Parser parse, ...}) =>
-          Parse.!!! (command_marker -- parse) >> (op |>)
+          Parse.!!! (command_markers -- parse) >> (op |>)
       | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
           before_command :|-- (fn restricted =>
-            Parse.!!! (command_marker -- parse restricted)) >> (op |>)
+            Parse.!!! (command_markers -- parse restricted)) >> (op |>)
       | NONE =>
           Scan.fail_with (fn _ => fn _ =>
             let
               val msg =
                 if Config.get_global thy bootstrap

             in msg ^ quote (Markup.markup Markup.keyword1 name) end))
     end);
 
 in
 
-fun parse_tokens thy =
-  filter Token.is_proper
-  #> Source.of_list
-  #> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs))
-  #> Source.exhaust;
-
-fun parse thy pos text =
+fun parse_span thy init span =
+  let
+    val range = Token.range_of span;
+    val core_range = Token.core_range_of span;
+
+    val markers = map Token.input_of (filter Token.is_document_marker span);
+    fun parse () =
+      filter Token.is_proper span
+      |> Source.of_list
+      |> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy markers) xs))
+      |> Source.exhaust;
+  in
+    (case parse () of
+      [tr] => Toplevel.modify_init init tr
+    | [] => Toplevel.ignored (#1 range)
+    | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
+    handle ERROR msg => Toplevel.malformed (#1 core_range) msg
+  end;
+
+fun parse_text thy init pos text =
   Symbol_Pos.explode (text, pos)
   |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false}
-  |> parse_tokens thy;
+  |> parse_spans
+  |> map (Command_Span.content #> parse_span thy init);
 
 end;
-
-
-(* parse spans *)
-
-local
-
-fun ship span =
-  let
-    val kind =
-      if forall Token.is_ignored span then Command_Span.Ignored_Span
-      else if exists Token.is_error span then Command_Span.Malformed_Span
-      else
-        (case find_first Token.is_command span of
-          NONE => Command_Span.Malformed_Span
-        | SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd));
-  in cons (Command_Span.Span (kind, span)) end;
-
-fun flush (result, content, ignored) =
-  result
-  |> not (null content) ? ship (rev content)
-  |> not (null ignored) ? ship (rev ignored);
-
-fun parse tok (result, content, ignored) =
-  if Token.is_ignored tok then (result, content, tok :: ignored)
-  else if Token.is_command_modifier tok orelse
-    Token.is_command tok andalso
-      (not (exists Token.is_command_modifier content) orelse exists Token.is_command content)
-  then (flush (result, content, ignored), [tok], [])
-  else (result, tok :: (ignored @ content), []);
-
-in
-
-fun parse_spans toks =
-  fold parse toks ([], [], []) |> flush |> rev;
-
-end;
-
-fun make_span toks =
-  (case parse_spans toks of
-    [span] => span
-  | _ => Command_Span.Span (Command_Span.Malformed_Span, toks));
 
 
 (* check commands *)
 
 fun command_reports thy tok =