# HG changeset patch
# User wenzelm
# Date 1552248749 -3600
# Node ID def3ec9cdb7e06774013b523f7e301ef425e5d12
# Parent  cb643a1a53134b812520819dee4cc7eefd9327d6
document markers are formal comments, and may thus occur anywhere in the command-span;
clarified Outer_Syntax.parse_span, Outer_Syntax.parse_text wrt. span structure;
tuned signature;

diff -r cb643a1a5313 -r def3ec9cdb7e etc/symbols
--- a/etc/symbols	Sun Mar 10 15:31:24 2019 +0100
+++ b/etc/symbols	Sun Mar 10 21:12:29 2019 +0100
@@ -359,9 +359,9 @@
 \<hole>                 code: 0x002311
 \<newline>              code: 0x0023ce
 \<comment>              code: 0x002015  group: document  argument: space_cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
-\<marker>               code: 0x002710  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
 \<^cancel>              code: 0x002326  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
 \<^latex>                               group: document  argument: cartouche
+\<^marker>              code: 0x002710  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
 \<open>                 code: 0x002039  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: <<
 \<close>                code: 0x00203a  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: >>
 \<^here>                code: 0x002302  font: Isabelle␣DejaVu␣Sans␣Mono
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/General/antiquote.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -122,12 +122,12 @@
   scan_nl || Scan.repeats1 scan_plain_txt @@@ scan_nl_opt;
 
 val scan_text_comments =
-  scan_nl || Scan.repeats1 (Comment.scan >> #2 || scan_plain_txt) @@@ scan_nl_opt;
+  scan_nl || Scan.repeats1 (Comment.scan_inner >> #2 || scan_plain_txt) @@@ scan_nl_opt;
 
 val scan_antiq_body =
   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
   Symbol_Pos.scan_cartouche err_prefix ||
-  Comment.scan --
+  Comment.scan_inner --
     Symbol_Pos.!!! (fn () => err_prefix ^ "bad formal comment in antiquote body") Scan.fail
     >> K [] ||
   Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/General/comment.ML
--- a/src/Pure/General/comment.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/General/comment.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -6,13 +6,15 @@
 
 signature COMMENT =
 sig
-  datatype kind = Comment | Cancel | Latex
+  datatype kind = Comment | Cancel | Latex | Marker
   val markups: kind -> Markup.T list
   val is_symbol: Symbol.symbol -> bool
   val scan_comment: (kind * Symbol_Pos.T list) scanner
   val scan_cancel: (kind * Symbol_Pos.T list) scanner
   val scan_latex: (kind * Symbol_Pos.T list) scanner
-  val scan: (kind * Symbol_Pos.T list) scanner
+  val scan_marker: (kind * Symbol_Pos.T list) scanner
+  val scan_inner: (kind * Symbol_Pos.T list) scanner
+  val scan_outer: (kind * Symbol_Pos.T list) scanner
   val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list
 end;
 
@@ -21,7 +23,7 @@
 
 (* kinds *)
 
-datatype kind = Comment | Cancel | Latex;
+datatype kind = Comment | Cancel | Latex | Marker;
 
 val kinds =
   [(Comment,
@@ -32,7 +34,10 @@
       markups = [Markup.language_text true]}),
    (Latex,
      {symbol = Symbol.latex, blanks = false,
-      markups = [Markup.language_latex true, Markup.no_words]})];
+      markups = [Markup.language_latex true, Markup.no_words]}),
+   (Marker,
+     {symbol = Symbol.marker, blanks = false,
+      markups = [Markup.language_document_marker]})];
 
 val get_kind = the o AList.lookup (op =) kinds;
 val print_kind = quote o #symbol o get_kind;
@@ -69,7 +74,10 @@
 val scan_comment = scan_strict Comment;
 val scan_cancel = scan_strict Cancel;
 val scan_latex = scan_strict Latex;
-val scan = scan_comment || scan_cancel || scan_latex;
+val scan_marker = scan_strict Marker;
+
+val scan_inner = scan_comment || scan_cancel || scan_latex;
+val scan_outer = scan_inner || scan_marker;
 
 val scan_body =
   Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE ||
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/General/comment.scala
--- a/src/Pure/General/comment.scala	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/General/comment.scala	Sun Mar 10 21:12:29 2019 +0100
@@ -14,12 +14,14 @@
     val COMMENT = Value("formal comment")
     val CANCEL = Value("canceled text")
     val LATEX = Value("embedded LaTeX")
+    val MARKER = Value("document marker")
   }
 
   lazy val symbols: Set[Symbol.Symbol] =
     Set(Symbol.comment, Symbol.comment_decoded,
       Symbol.cancel, Symbol.cancel_decoded,
-      Symbol.latex, Symbol.latex_decoded)
+      Symbol.latex, Symbol.latex_decoded,
+      Symbol.marker, Symbol.marker_decoded)
 
   lazy val symbols_blanks: Set[Symbol.Symbol] =
     Set(Symbol.comment, Symbol.comment_decoded)
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/General/symbol.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -18,6 +18,7 @@
   val comment: symbol
   val cancel: symbol
   val latex: symbol
+  val marker: symbol
   val is_char: symbol -> bool
   val is_utf8: symbol -> bool
   val is_symbolic: symbol -> bool
@@ -120,6 +121,7 @@
 val comment = "\<comment>";
 val cancel = "\<^cancel>";
 val latex = "\<^latex>";
+val marker = "\<^marker>";
 
 fun is_char s = size s = 1;
 
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/General/symbol.scala	Sun Mar 10 21:12:29 2019 +0100
@@ -493,10 +493,10 @@
     /* misc symbols */
 
     val newline_decoded = decode(newline)
-    val marker_decoded = decode(marker)
     val comment_decoded = decode(comment)
     val cancel_decoded = decode(cancel)
     val latex_decoded = decode(latex)
+    val marker_decoded = decode(marker)
     val open_decoded = decode(open)
     val close_decoded = decode(close)
 
@@ -579,23 +579,17 @@
     else str
 
 
-  /* marker */
-
-  val marker: Symbol = "\\<marker>"
-  def marker_decoded: Symbol = symbols.marker_decoded
-
-  lazy val is_marker: Set[Symbol] = Set(marker, marker_decoded)
-
-
   /* formal comments */
 
   val comment: Symbol = "\\<comment>"
   val cancel: Symbol = "\\<^cancel>"
   val latex: Symbol = "\\<^latex>"
+  val marker: Symbol = "\\<^marker>"
 
   def comment_decoded: Symbol = symbols.comment_decoded
   def cancel_decoded: Symbol = symbols.cancel_decoded
   def latex_decoded: Symbol = symbols.latex_decoded
+  def marker_decoded: Symbol = symbols.marker_decoded
 
 
   /* cartouches */
diff -r cb643a1a5313 -r def3ec9cdb7e 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 =
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Isar/parse.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -96,6 +96,7 @@
   val for_fixes: (binding * string option * mixfix) list parser
   val ML_source: Input.source parser
   val document_source: Input.source parser
+  val document_marker: Input.source parser
   val const: string parser
   val term: string parser
   val prop: string parser
@@ -390,6 +391,10 @@
 val ML_source = input (group (fn () => "ML source") text);
 val document_source = input (group (fn () => "document source") text);
 
+val document_marker =
+  group (fn () => "document marker")
+    (RESET_VALUE (Scan.one Token.is_document_marker >> Token.input_of));
+
 
 (* terms *)
 
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Isar/parse.scala	Sun Mar 10 21:12:29 2019 +0100
@@ -83,10 +83,9 @@
     def tag: Parser[String] = $$$("%") ~> tag_name
     def tags: Parser[List[String]] = rep(tag)
 
-    def marker: Parser[String] =
-      ($$$(Symbol.marker) | $$$(Symbol.marker_decoded)) ~! embedded ^^ { case _ ~ x => x }
+    def marker: Parser[String] = token("marker", _.is_marker) ^^ (_.content)
 
-    def annotation: Parser[Unit] = rep(marker | tag) ^^ { case _ => () }
+    def annotation: Parser[Unit] = rep(tag | marker) ^^ { case _ => () }
 
 
     /* wrappers */
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Isar/token.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -30,7 +30,6 @@
     Declaration of declaration |
     Files of file Exn.result list
   val pos_of: T -> Position.T
-  val range_of: T list -> Position.range
   val adjust_offsets: (int -> int option) -> T -> T
   val eof: T
   val is_eof: T -> bool
@@ -46,6 +45,7 @@
   val is_comment: T -> bool
   val is_informal_comment: T -> bool
   val is_formal_comment: T -> bool
+  val is_document_marker: T -> bool
   val is_ignored: T -> bool
   val is_begin_ignore: T -> bool
   val is_end_ignore: T -> bool
@@ -53,6 +53,8 @@
   val is_space: T -> bool
   val is_blank: T -> bool
   val is_newline: T -> bool
+  val range_of: T list -> Position.range
+  val core_range_of: T list -> Position.range
   val content_of: T -> string
   val source_of: T -> string
   val input_of: T -> Input.source
@@ -190,11 +192,6 @@
 fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
 fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
 
-fun range_of (toks as tok :: _) =
-      let val pos' = end_pos_of (List.last toks)
-      in Position.range (pos_of tok, pos') end
-  | range_of [] = Position.no_range;
-
 fun adjust_offsets adjust (Token ((x, range), y, z)) =
   Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
 
@@ -245,6 +242,9 @@
 fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true
   | is_formal_comment _ = false;
 
+fun is_document_marker (Token (_, (Comment (SOME Comment.Marker), _), _)) = true
+  | is_document_marker _ = false;
+
 fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true
   | is_begin_ignore _ = false;
 
@@ -267,6 +267,17 @@
   | is_newline _ = false;
 
 
+(* range of tokens *)
+
+fun range_of (toks as tok :: _) =
+      let val pos' = end_pos_of (List.last toks)
+      in Position.range (pos_of tok, pos') end
+  | range_of [] = Position.no_range;
+
+val core_range_of =
+  drop_prefix is_ignored #> drop_suffix is_ignored #> range_of;
+
+
 (* token content *)
 
 fun content_of (Token (_, (_, x), _)) = x;
@@ -636,7 +647,7 @@
     scan_verbatim >> token_range Verbatim ||
     scan_cartouche >> token_range Cartouche ||
     scan_comment >> token_range (Comment NONE) ||
-    Comment.scan >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
+    Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
     scan_space >> token Space ||
     (Scan.max token_leq
       (Scan.max token_leq
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Isar/token.scala	Sun Mar 10 21:12:29 2019 +0100
@@ -304,6 +304,9 @@
   def is_space: Boolean = kind == Token.Kind.SPACE
   def is_informal_comment: Boolean = kind == Token.Kind.INFORMAL_COMMENT
   def is_formal_comment: Boolean = kind == Token.Kind.FORMAL_COMMENT
+  def is_marker: Boolean =
+    kind == Token.Kind.FORMAL_COMMENT &&
+    (source.startsWith(Symbol.marker) || source.startsWith(Symbol.marker_decoded))
   def is_comment: Boolean = is_informal_comment || is_formal_comment
   def is_ignored: Boolean = is_space || is_informal_comment
   def is_proper: Boolean = !is_space && !is_comment
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -312,7 +312,7 @@
 val scan_sml_antiq = scan_sml >> Antiquote.Text;
 
 val scan_ml_antiq =
-  Comment.scan >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
+  Comment.scan_inner >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
   Antiquote.scan_control >> Antiquote.Control ||
   Antiquote.scan_antiq >> Antiquote.Antiq ||
   scan_rat_antiq >> Antiquote.Antiq ||
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/PIDE/command.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -155,12 +155,7 @@
         Position.here_list verbatim);
   in
     if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax"
-    else
-      (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
-        [tr] => Toplevel.modify_init init tr
-      | [] => Toplevel.ignored (#1 (Token.range_of span))
-      | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
-      handle ERROR msg => Toplevel.malformed (#1 core_range) msg
+    else Outer_Syntax.parse_span thy init (resolve_files keywords master_dir blobs_info span)
   end;
 
 end;
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Mar 10 21:12:29 2019 +0100
@@ -475,7 +475,6 @@
       toks match {
         case (t1, i1) :: (t2, i2) :: rest =>
           if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest)
-          else if (t1.is_keyword && Symbol.is_marker(t1.source) && t2.is_embedded) clean(rest)
           else (t1, i1) :: clean((t2, i2) :: rest)
         case _ => toks
       }
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Pure.thy	Sun Mar 10 21:12:29 2019 +0100
@@ -7,7 +7,7 @@
 theory Pure
 keywords
     "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
-    "\<marker>" "\<subseteq>" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
+    "\<subseteq>" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
     "overloaded" "pervasive" "premises" "structure" "unchecked"
   and "private" "qualified" :: before_command
   and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -301,7 +301,7 @@
 
     val scan =
       Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
-      Comment.scan >> (fn (kind, ss) => token (Comment kind) ss) ||
+      Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) ||
       Scan.max token_leq scan_lit scan_val ||
       scan_string >> token String ||
       scan_str >> token Str ||
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/Thy/document_marker.ML
--- a/src/Pure/Thy/document_marker.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Thy/document_marker.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -10,6 +10,7 @@
   val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
   val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory
   val evaluate: Input.source -> marker
+  val legacy_tag: string -> Input.source
 end;
 
 structure Document_Marker: DOCUMENT_MARKER =
@@ -47,14 +48,14 @@
 
 fun evaluate input ctxt =
   let
-    val pos = Input.pos_of input;
-    val _ = Context_Position.report ctxt pos Markup.language_document_marker;
-
-    val syms = Input.source_explode input;
+    val body =
+      Input.source_explode input
+      |> drop_prefix (fn (s, _) => s = Symbol.marker)
+      |> Symbol_Pos.cartouche_content;
     val markers =
-      (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) syms of
+      (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) body of
         SOME res => res
-      | NONE => error ("Bad input" ^ Position.here pos));
+      | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)));
   in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end;
 
 
@@ -77,4 +78,7 @@
           val _ = Context_Position.report ctxt pos Markup.words;
         in meta_data Markup.meta_description arg ctxt end));
 
+fun legacy_tag name =
+  Input.string (cartouche ("tag " ^ Symbol_Pos.quote_string_qq name));
+
 end;
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/Thy/document_source.ML
--- a/src/Pure/Thy/document_source.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Thy/document_source.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -17,7 +17,7 @@
   val get_tags: Proof.context -> string list
   val update_tags: string -> Proof.context -> Proof.context
   val tags: string list parser
-  val annotation: Input.source list parser
+  val annotation: unit parser
 end;
 
 structure Document_Source: DOCUMENT_SOURCE =
@@ -62,13 +62,8 @@
 
 (* semantic markers (operation on presentation context) *)
 
-val marker =
-  (improper -- Parse.$$$ "\<marker>" -- improper) |--
-    Parse.!!! (Parse.group (fn () => "document marker") (Parse.input Parse.embedded) --| blank_end);
+val marker = improper |-- Parse.document_marker --| blank_end;
 
-val tag_marker =  (*emulation of old-style tags*)
-  tag >> (fn name => Input.string ("tag " ^ Symbol_Pos.quote_string_qq name));
-
-val annotation = Scan.repeat (marker || tag_marker);
+val annotation = Scan.repeat (tag >> K () || marker >> K ()) >> K ();
 
 end;
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -175,10 +175,10 @@
     Parse.command_name textN ||
     Parse.command_name txtN ||
     Parse.command_name text_rawN) --
-  Document_Source.annotation -- Parse.!!! Parse.document_source;
+  (Document_Source.annotation |-- Parse.!!! Parse.document_source);
 
 val parse_header =
-  (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.annotation)
+  (Scan.repeat heading -- Parse.command_name theoryN --| Document_Source.annotation)
     |-- Parse.!!! args;
 
 fun read_tokens pos toks =
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -451,9 +451,7 @@
 
 fun script_thy pos txt thy =
   let
-    val trs =
-      Outer_Syntax.parse thy pos txt
-      |> map (Toplevel.modify_init (K thy));
+    val trs = Outer_Syntax.parse_text thy (K thy) pos txt;
     val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
     val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
   in Toplevel.end_theory end_pos end_state end;
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -61,8 +61,8 @@
       Symbol_Pos.cartouche_content syms
       |> output_symbols
       |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
-  | Comment.Latex =>
-      [Latex.symbols (Symbol_Pos.cartouche_content syms)])
+  | Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)]
+  | Comment.Marker => [])
 and output_comment_document ctxt (comment, syms) =
   (case comment of
     SOME kind => output_comment ctxt (kind, syms)
@@ -139,6 +139,7 @@
   in
     (case Token.kind_of tok of
       Token.Comment NONE => []
+    | Token.Comment (SOME Comment.Marker) => []
     | Token.Command => output false "\\isacommand{" "}"
     | Token.Keyword =>
         if Symbol.is_ascii_identifier (Token.content_of tok)
diff -r cb643a1a5313 -r def3ec9cdb7e src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Tools/rail.ML	Sun Mar 10 21:12:29 2019 +0100
@@ -118,7 +118,7 @@
 
 val scan_token =
   scan_space >> token Space ||
-  Comment.scan >> (fn (kind, ss) => token (Comment kind) ss)||
+  Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) ||
   Antiquote.scan_antiq >> antiq_token ||
   scan_keyword >> (token Keyword o single) ||
   Lexicon.scan_id >> token Ident ||