src/Pure/Isar/outer_syntax.ML

--- a/src/Pure/Isar/outer_syntax.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -22,10 +22,10 @@
   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;
@@ -172,60 +172,6 @@
 
 (** toplevel parsing **)
 
-(* 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 =
-  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);
-    in
-      (case lookup_commands thy name of
-        SOME (Command {command_parser = Parser parse, ...}) =>
-          Parse.!!! (command_marker -- parse) >> (op |>)
-      | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
-          before_command :|-- (fn restricted =>
-            Parse.!!! (command_marker -- parse restricted)) >> (op |>)
-      | NONE =>
-          Scan.fail_with (fn _ => fn _ =>
-            let
-              val msg =
-                if Config.get_global thy bootstrap
-                then "missing theory context for command "
-                else "undefined command ";
-            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 =
-  Symbol_Pos.explode (text, pos)
-  |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false}
-  |> parse_tokens thy;
-
-end;
-
-
 (* parse spans *)
 
 local
@@ -267,6 +213,75 @@
   | _ => 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 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_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_markers -- parse) >> (op |>)
+      | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
+          before_command :|-- (fn restricted =>
+            Parse.!!! (command_markers -- parse restricted)) >> (op |>)
+      | NONE =>
+          Scan.fail_with (fn _ => fn _ =>
+            let
+              val msg =
+                if Config.get_global thy bootstrap
+                then "missing theory context for command "
+                else "undefined command ";
+            in msg ^ quote (Markup.markup Markup.keyword1 name) end))
+    end);
+
+in
+
+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_spans
+  |> map (Command_Span.content #> parse_span thy init);
+
+end;
+
+
 (* check commands *)
 
 fun command_reports thy tok =