added semantic document markers;
emulate old-style tags as "tag" markers, with subtle change of semantics for multiples tags (ever used?);
tuned;

--- a/src/Pure/General/symbol.scala	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/General/symbol.scala	Sun Mar 10 00:21:34 2019 +0100
@@ -493,6 +493,7 @@
     /* 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)
@@ -578,6 +579,14 @@
     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>"

--- a/src/Pure/Isar/outer_syntax.ML	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sun Mar 10 00:21:34 2019 +0100
@@ -185,20 +185,21 @@
   Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
     let
       val keywords = Thy_Header.get_keywords thy;
-      val command_tags = Parse.command -- Document_Source.tags;
       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_tags |-- parse) >> (fn f => f tr0)
+          Parse.!!! (command_marker -- parse) >> (op |>)
       | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
           before_command :|-- (fn restricted =>
-            Parse.!!! (command_tags |-- parse restricted)) >> (fn f => f tr0)
+            Parse.!!! (command_marker -- parse restricted)) >> (op |>)
       | NONE =>
           Scan.fail_with (fn _ => fn _ =>
             let

--- a/src/Pure/Isar/parse.scala	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/Isar/parse.scala	Sun Mar 10 00:21:34 2019 +0100
@@ -80,7 +80,13 @@
           tok.kind == Token.Kind.IDENT ||
           tok.kind == Token.Kind.STRING)
 
-    def tags: Parser[List[String]] = rep($$$("%") ~> tag_name)
+    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 annotation: Parser[Unit] = rep(marker | tag) ^^ { case _ => () }
 
 
     /* wrappers */

--- a/src/Pure/Isar/toplevel.ML	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sun Mar 10 00:21:34 2019 +0100
@@ -37,6 +37,7 @@
   val type_error: transition -> string
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
+  val markers: Input.source list -> transition -> transition
   val timing: Time.time -> transition -> transition
   val init_theory: (unit -> theory) -> transition -> transition
   val is_init: transition -> bool
@@ -85,6 +86,7 @@
   val reset_theory: state -> state option
   val reset_proof: state -> state option
   val reset_notepad: state -> state option
+  val fork_presentation: transition -> transition * transition
   type result
   val join_results: result -> (transition * state) list
   val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state
@@ -142,12 +144,9 @@
 fun node_of (State ((node, _), _)) = node;
 fun previous_theory_of (State (_, prev_thy)) = prev_thy;
 
-fun init_toplevel () =
-  let val thy0 = Theory.get_pure () handle Fail _ => Context.the_global_context ();
-  in State ((Toplevel, Proof_Context.init_global thy0), NONE) end;
+fun init_toplevel () = State (node_presentation Toplevel, NONE);
+fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE);
 
-fun theory_toplevel thy =
-  State (node_presentation (Theory (Context.Theory thy)), NONE);
 
 fun level state =
   (case node_of state of
@@ -289,22 +288,24 @@
 
 local
 
-fun apply_tr _ (Init f) (State ((Toplevel, _), _)) =
-      let val node = Theory (Context.Theory (Runtime.controlled_execution NONE f ()))
-      in State (node_presentation node, NONE) end
-  | apply_tr _ Exit (State ((node as Theory (Context.Theory thy), _), _)) =
+fun apply_tr int trans state =
+  (case (trans, node_of state) of
+    (Init f, Toplevel) =>
+      Runtime.controlled_execution NONE (fn () =>
+        State (node_presentation (Theory (Context.Theory (f ()))), NONE)) ()
+  | (Exit, node as Theory (Context.Theory thy)) =>
       let
         val State ((node', pr_ctxt), _) =
           node |> apply_transaction
             (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy))))
             (K ());
       in State ((Toplevel, pr_ctxt), get_theory node') end
-  | apply_tr int (Keep f) state =
-      Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
-  | apply_tr _ (Transaction _) (State ((Toplevel, _), _)) = raise UNDEF
-  | apply_tr int (Transaction (f, g)) (State ((node, _), _)) =
-      apply_transaction (fn x => f int x) g node
-  | apply_tr _ _ _ = raise UNDEF;
+  | (Keep f, node) =>
+      Runtime.controlled_execution (try generic_theory_of state)
+        (fn () => (f int state; State (node_presentation node, previous_theory_of state))) ()
+  | (Transaction _, Toplevel) => raise UNDEF
+  | (Transaction (f, g), node) => apply_transaction (fn x => f int x) g node
+  | _ => raise UNDEF);
 
 fun apply_union _ [] state = raise FAILURE (state, UNDEF)
   | apply_union int (tr :: trs) state =
@@ -314,9 +315,18 @@
           | exn as FAILURE _ => raise exn
           | exn => raise FAILURE (state, exn);
 
+fun apply_markers markers (state as State ((node, pr_ctxt), prev_thy)) =
+  let
+    val state' =
+      Runtime.controlled_execution (try generic_theory_of state)
+        (fn () => State ((node, fold Document_Marker.evaluate markers pr_ctxt), prev_thy)) ();
+  in (state', NONE) end
+  handle exn => (state, SOME exn);
+
 in
 
-fun apply_trans int trs state = (apply_union int trs state, NONE)
+fun apply_trans int trans markers state =
+  (apply_union int trans state |> apply_markers markers)
   handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
 
 end;
@@ -325,18 +335,19 @@
 (* datatype transition *)
 
 datatype transition = Transition of
- {name: string,              (*command name*)
-  pos: Position.T,           (*source position*)
-  timing: Time.time,         (*prescient timing information*)
-  trans: trans list};        (*primitive transitions (union)*)
+ {name: string,               (*command name*)
+  pos: Position.T,            (*source position*)
+  markers: Input.source list, (*semantic document markers*)
+  timing: Time.time,          (*prescient timing information*)
+  trans: trans list};         (*primitive transitions (union)*)
 
-fun make_transition (name, pos, timing, trans) =
-  Transition {name = name, pos = pos, timing = timing, trans = trans};
+fun make_transition (name, pos, markers, timing, trans) =
+  Transition {name = name, pos = pos, markers = markers, timing = timing, trans = trans};
 
-fun map_transition f (Transition {name, pos, timing, trans}) =
-  make_transition (f (name, pos, timing, trans));
+fun map_transition f (Transition {name, pos, markers, timing, trans}) =
+  make_transition (f (name, pos, markers, timing, trans));
 
-val empty = make_transition ("", Position.none, Time.zeroTime, []);
+val empty = make_transition ("", Position.none, [], Time.zeroTime, []);
 
 
 (* diagnostics *)
@@ -355,20 +366,23 @@
 
 (* modify transitions *)
 
-fun name name = map_transition (fn (_, pos, timing, trans) =>
-  (name, pos, timing, trans));
+fun name name = map_transition (fn (_, pos, markers, timing, trans) =>
+  (name, pos, markers, timing, trans));
 
-fun position pos = map_transition (fn (name, _, timing, trans) =>
-  (name, pos, timing, trans));
+fun position pos = map_transition (fn (name, _, markers, timing, trans) =>
+  (name, pos, markers, timing, trans));
+
+fun markers markers = map_transition (fn (name, pos, _, timing, trans) =>
+  (name, pos, markers, timing, trans));
 
-fun timing timing = map_transition (fn (name, pos, _, trans) =>
-  (name, pos, timing, trans));
+fun timing timing = map_transition (fn (name, pos, markers, _, trans) =>
+  (name, pos, markers, timing, trans));
 
-fun add_trans tr = map_transition (fn (name, pos, timing, trans) =>
-  (name, pos, timing, tr :: trans));
+fun add_trans tr = map_transition (fn (name, pos, markers, timing, trans) =>
+  (name, pos, markers, timing, tr :: trans));
 
-val reset_trans = map_transition (fn (name, pos, timing, _) =>
-  (name, pos, timing, []));
+val reset_trans = map_transition (fn (name, pos, markers, timing, _) =>
+  (name, pos, markers, timing, []));
 
 
 (* basic transitions *)
@@ -605,9 +619,9 @@
 
 local
 
-fun app int (tr as Transition {trans, ...}) =
+fun app int (tr as Transition {markers, trans, ...}) =
   setmp_thread_position tr
-    (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans)
+    (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans markers)
       ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn));
 
 in
@@ -707,18 +721,26 @@
         then Future.proofs_enabled 1
         else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate));
 
+val empty_markers = markers [];
+val empty_trans = reset_trans #> keep (K ());
+
+in
+
+fun fork_presentation tr = (tr |> empty_markers, tr |> empty_trans);
+
 fun atom_result keywords tr st =
   let
     val st' =
       if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
-        (Execution.fork
-          {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
-          (fn () => command tr st); st)
+        let
+          val (tr1, tr2) = fork_presentation tr;
+          val _ =
+            Execution.fork {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
+              (fn () => command tr1 st);
+        in command tr2 st end
       else command tr st;
   in (Result (tr, st'), st') end;
 
-in
-
 fun element_result keywords (Thy_Element.Element (tr, NONE)) st = atom_result keywords tr st
   | element_result keywords (elem as Thy_Element.Element (head_tr, SOME element_rest)) st =
       let
@@ -734,6 +756,8 @@
           in (Result_List (head_result :: proof_results), st'') end
         else
           let
+            val (end_tr1, end_tr2) = fork_presentation end_tr;
+
             val finish = Context.Theory o Proof_Context.theory_of;
 
             val future_proof =
@@ -744,10 +768,10 @@
                     let
                       val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st';
                       val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy));
-                      val (result, result_state) =
+                      val (results, result_state) =
                         State (node_presentation node', prev_thy)
-                        |> fold_map (element_result keywords) body_elems ||> command end_tr;
-                    in (Result_List result, presentation_context0 result_state) end))
+                        |> fold_map (element_result keywords) body_elems ||> command end_tr1;
+                    in (Result_List results, presentation_context0 result_state) end))
               #> (fn (res, state') => state' |> put_result (Result_Future res));
 
             val forked_proof =
@@ -756,12 +780,12 @@
               end_proof (fn _ => future_proof #>
                 (fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
 
-            val st'' = st'
-              |> command (head_tr |> reset_trans |> forked_proof);
-            val end_result = Result (end_tr, st'');
+            val st'' = st' |> command (head_tr |> reset_trans |> forked_proof);
+            val end_st = st'' |> command end_tr2;
+            val end_result = Result (end_tr, end_st);
             val result =
               Result_List [head_result, Result.get (presentation_context0 st''), end_result];
-          in (result, st'') end
+          in (result, end_st) end
       end;
 
 end;

--- a/src/Pure/PIDE/command.ML	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/PIDE/command.ML	Sun Mar 10 00:21:34 2019 +0100
@@ -217,8 +217,12 @@
 
 fun run keywords int tr st =
   if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
-    (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
-      (fn () => Toplevel.command_exception int tr st); ([], SOME st))
+    let
+      val (tr1, tr2) = Toplevel.fork_presentation tr;
+      val _ =
+        Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
+          (fn () => Toplevel.command_exception int tr1 st);
+    in Toplevel.command_errors int tr2 st end
   else Toplevel.command_errors int tr st;
 
 fun check_token_comments ctxt tok =

--- a/src/Pure/PIDE/command.scala	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Mar 10 00:21:34 2019 +0100
@@ -475,6 +475,7 @@
       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
       }

--- a/src/Pure/PIDE/markup.ML	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun Mar 10 00:21:34 2019 +0100
@@ -32,6 +32,7 @@
   val language_ML: bool -> T
   val language_SML: bool -> T
   val language_document: bool -> T
+  val language_document_marker: T
   val language_antiquotation: T
   val language_text: bool -> T
   val language_verbatim: bool -> T
@@ -314,6 +315,8 @@
 val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
 val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
 val language_document = language' {name = "document", symbols = false, antiquotes = true};
+val language_document_marker =
+  language {name = "document_marker", symbols = true, antiquotes = true, delimited = true};
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
 val language_text = language' {name = "text", symbols = true, antiquotes = false};

--- a/src/Pure/Pure.thy	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/Pure.thy	Sun Mar 10 00:21:34 2019 +0100
@@ -7,7 +7,7 @@
 theory Pure
 keywords
     "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
-    "\<subseteq>" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
+    "\<marker>" "\<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"

--- a/src/Pure/ROOT.ML	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/ROOT.ML	Sun Mar 10 00:21:34 2019 +0100
@@ -208,6 +208,7 @@
 ML_file "Isar/parse.ML";
 ML_file "Thy/document_source.ML";
 ML_file "Thy/thy_header.ML";
+ML_file "Thy/document_marker.ML";
 
 (*proof context*)
 ML_file "Isar/object_logic.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/document_marker.ML	Sun Mar 10 00:21:34 2019 +0100
@@ -0,0 +1,64 @@
+(*  Title:      Pure/Thy/document_marker.ML
+    Author:     Makarius
+
+Document markers: declarations on the presentation context.
+*)
+
+signature DOCUMENT_MARKER =
+sig
+  type marker = Proof.context -> Proof.context
+  val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
+  val evaluate: Input.source -> marker
+end;
+
+structure Document_Marker: DOCUMENT_MARKER =
+struct
+
+(* theory data *)
+
+type marker = Proof.context -> Proof.context;
+
+structure Markers = Theory_Data
+(
+  type T = (Token.src -> Proof.context -> Proof.context) Name_Space.table;
+  val empty : T = Name_Space.empty_table "document_marker";
+  val extend = I;
+  val merge = Name_Space.merge_tables;
+);
+
+val get_markers = Markers.get o Proof_Context.theory_of;
+
+fun check ctxt = Name_Space.check (Context.Proof ctxt) (get_markers ctxt);
+
+fun setup name scan body thy =
+  let
+    fun marker src ctxt =
+      let val (x, ctxt') = Token.syntax scan src ctxt
+      in body x ctxt' end;
+  in thy |> Markers.map (Name_Space.define (Context.Theory thy) true (name, marker) #> #2) end;
+
+
+(* evaluate inner syntax *)
+
+val parse_marker = Parse.token Parse.liberal_name ::: Parse.!!! Parse.args;
+
+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 markers =
+      (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) syms of
+        SOME res => res
+      | NONE => error ("Bad input" ^ Position.here pos));
+  in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end;
+
+
+(* concrete markers *)
+
+val _ =
+  Theory.setup
+    (setup (Binding.make ("tag", \<^here>)) (Scan.lift Parse.name) Document_Source.update_tags);
+
+end;

--- a/src/Pure/Thy/document_source.ML	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/Thy/document_source.ML	Sun Mar 10 00:21:34 2019 +0100
@@ -14,8 +14,10 @@
   val improper: Token.T list parser
   val improper_end: Token.T list parser
   val blank_end: Token.T list parser
-  val tag: string parser
+  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
 end;
 
 structure Document_Source: DOCUMENT_SOURCE =
@@ -41,11 +43,32 @@
 val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
 
 
-(* tags *)
+(* syntactic tags (old-style) *)
+
+structure Tags = Proof_Data
+(
+  type T = string list;
+  fun init _ = [];
+);
+
+val get_tags = Tags.get;
+val update_tags = Tags.map o update (op =);
 
 val tag_name = Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string);
 
 val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (tag_name --| blank_end);
 val tags = Scan.repeat tag;
 
+
+(* 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 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);
+
 end;

--- a/src/Pure/Thy/thy_header.ML	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sun Mar 10 00:21:34 2019 +0100
@@ -175,10 +175,11 @@
     Parse.command_name textN ||
     Parse.command_name txtN ||
     Parse.command_name text_rawN) --
-  Document_Source.tags -- Parse.!!! Parse.document_source;
+  Document_Source.annotation -- Parse.!!! Parse.document_source;
 
 val parse_header =
-  (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.tags) |-- Parse.!!! args;
+  (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.annotation)
+    |-- Parse.!!! args;
 
 fun read_tokens pos toks =
   filter Token.is_proper toks

--- a/src/Pure/Thy/thy_header.scala	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Mar 10 00:21:34 2019 +0100
@@ -172,9 +172,9 @@
           command(TEXT) |
           command(TXT) |
           command(TEXT_RAW)) ~
-        tags ~! document_source
+        annotation ~! document_source
 
-      (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
+      (rep(heading) ~ command(THEORY) ~ annotation) ~! args ^^ { case _ ~ x => x }
     }
   }
 

--- a/src/Pure/Thy/thy_output.ML	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Mar 10 00:21:34 2019 +0100
@@ -202,7 +202,7 @@
 
 (* command spans *)
 
-type command = string * Position.T * string list;   (*name, position, tags*)
+type command = string * Position.T;   (*name, position*)
 type source = (token * (string * int)) list;        (*token, markup flag, meta-comment depth*)
 
 datatype span = Span of command * (source * source * source * source) * bool;
@@ -287,7 +287,8 @@
         #> cons (Latex.string flag)
       | _ => I);
 
-    val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
+    val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
+    val cmd_tags = Document_Source.get_tags (Toplevel.presentation_context state');
 
     val (tag, tags) = tag_stack;
     val {tag', active_tag'} =
@@ -371,19 +372,19 @@
       Document_Source.improper |--
         Parse.position (Scan.one (fn tok =>
           Token.is_command tok andalso pred keywords (Token.content_of tok))) --
-      Scan.repeat Document_Source.tag --
-      Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
-        Parse.document_source --| Document_Source.improper_end)
-          >> (fn (((tok, pos'), tags), source) =>
-            let val name = Token.content_of tok
-            in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
+      (Document_Source.annotation |--
+        Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
+          Parse.document_source --| Document_Source.improper_end))
+            >> (fn ((tok, pos'), source) =>
+              let val name = Token.content_of tok
+              in (SOME (name, pos'), (mk (name, source), (flag, d))) end));
 
     val command = Scan.peek (fn d =>
       Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
-      Scan.one Token.is_command -- Document_Source.tags
-      >> (fn ((cmd_mod, cmd), tags) =>
+      Scan.one Token.is_command --| Document_Source.annotation
+      >> (fn (cmd_mod, cmd) =>
         map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
-          [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
+          [(SOME (Token.content_of cmd, Token.pos_of cmd),
             (Basic_Token cmd, (markup_false, d)))]));
 
     val cmt = Scan.peek (fn d =>