added semantic document markers;
authorwenzelm
Sun Mar 10 00:21:34 2019 +0100 (3 months ago ago)
changeset 70068b9985133805d
parent 70067 0cb8753bdb50
child 70069 6db51f45b5f9
added semantic document markers;
emulate old-style tags as "tag" markers, with subtle change of semantics for multiples tags (ever used?);
tuned;
src/Pure/General/symbol.scala
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/parse.scala
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup.ML
src/Pure/Pure.thy
src/Pure/ROOT.ML
src/Pure/Thy/document_marker.ML
src/Pure/Thy/document_source.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/General/symbol.scala	Sat Mar 09 23:57:07 2019 +0100
     1.2 +++ b/src/Pure/General/symbol.scala	Sun Mar 10 00:21:34 2019 +0100
     1.3 @@ -493,6 +493,7 @@
     1.4      /* misc symbols */
     1.5  
     1.6      val newline_decoded = decode(newline)
     1.7 +    val marker_decoded = decode(marker)
     1.8      val comment_decoded = decode(comment)
     1.9      val cancel_decoded = decode(cancel)
    1.10      val latex_decoded = decode(latex)
    1.11 @@ -578,6 +579,14 @@
    1.12      else str
    1.13  
    1.14  
    1.15 +  /* marker */
    1.16 +
    1.17 +  val marker: Symbol = "\\<marker>"
    1.18 +  def marker_decoded: Symbol = symbols.marker_decoded
    1.19 +
    1.20 +  lazy val is_marker: Set[Symbol] = Set(marker, marker_decoded)
    1.21 +
    1.22 +
    1.23    /* formal comments */
    1.24  
    1.25    val comment: Symbol = "\\<comment>"
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Mar 09 23:57:07 2019 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Mar 10 00:21:34 2019 +0100
     2.3 @@ -185,20 +185,21 @@
     2.4    Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
     2.5      let
     2.6        val keywords = Thy_Header.get_keywords thy;
     2.7 -      val command_tags = Parse.command -- Document_Source.tags;
     2.8        val tr0 =
     2.9          Toplevel.empty
    2.10          |> Toplevel.name name
    2.11          |> Toplevel.position pos
    2.12          |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
    2.13          |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
    2.14 +      val command_marker =
    2.15 +        Parse.command |-- Document_Source.annotation >> (fn markers => Toplevel.markers markers tr0);
    2.16      in
    2.17        (case lookup_commands thy name of
    2.18          SOME (Command {command_parser = Parser parse, ...}) =>
    2.19 -          Parse.!!! (command_tags |-- parse) >> (fn f => f tr0)
    2.20 +          Parse.!!! (command_marker -- parse) >> (op |>)
    2.21        | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
    2.22            before_command :|-- (fn restricted =>
    2.23 -            Parse.!!! (command_tags |-- parse restricted)) >> (fn f => f tr0)
    2.24 +            Parse.!!! (command_marker -- parse restricted)) >> (op |>)
    2.25        | NONE =>
    2.26            Scan.fail_with (fn _ => fn _ =>
    2.27              let
     3.1 --- a/src/Pure/Isar/parse.scala	Sat Mar 09 23:57:07 2019 +0100
     3.2 +++ b/src/Pure/Isar/parse.scala	Sun Mar 10 00:21:34 2019 +0100
     3.3 @@ -80,7 +80,13 @@
     3.4            tok.kind == Token.Kind.IDENT ||
     3.5            tok.kind == Token.Kind.STRING)
     3.6  
     3.7 -    def tags: Parser[List[String]] = rep($$$("%") ~> tag_name)
     3.8 +    def tag: Parser[String] = $$$("%") ~> tag_name
     3.9 +    def tags: Parser[List[String]] = rep(tag)
    3.10 +
    3.11 +    def marker: Parser[String] =
    3.12 +      ($$$(Symbol.marker) | $$$(Symbol.marker_decoded)) ~! embedded ^^ { case _ ~ x => x }
    3.13 +
    3.14 +    def annotation: Parser[Unit] = rep(marker | tag) ^^ { case _ => () }
    3.15  
    3.16  
    3.17      /* wrappers */
     4.1 --- a/src/Pure/Isar/toplevel.ML	Sat Mar 09 23:57:07 2019 +0100
     4.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Mar 10 00:21:34 2019 +0100
     4.3 @@ -37,6 +37,7 @@
     4.4    val type_error: transition -> string
     4.5    val name: string -> transition -> transition
     4.6    val position: Position.T -> transition -> transition
     4.7 +  val markers: Input.source list -> transition -> transition
     4.8    val timing: Time.time -> transition -> transition
     4.9    val init_theory: (unit -> theory) -> transition -> transition
    4.10    val is_init: transition -> bool
    4.11 @@ -85,6 +86,7 @@
    4.12    val reset_theory: state -> state option
    4.13    val reset_proof: state -> state option
    4.14    val reset_notepad: state -> state option
    4.15 +  val fork_presentation: transition -> transition * transition
    4.16    type result
    4.17    val join_results: result -> (transition * state) list
    4.18    val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state
    4.19 @@ -142,12 +144,9 @@
    4.20  fun node_of (State ((node, _), _)) = node;
    4.21  fun previous_theory_of (State (_, prev_thy)) = prev_thy;
    4.22  
    4.23 -fun init_toplevel () =
    4.24 -  let val thy0 = Theory.get_pure () handle Fail _ => Context.the_global_context ();
    4.25 -  in State ((Toplevel, Proof_Context.init_global thy0), NONE) end;
    4.26 +fun init_toplevel () = State (node_presentation Toplevel, NONE);
    4.27 +fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE);
    4.28  
    4.29 -fun theory_toplevel thy =
    4.30 -  State (node_presentation (Theory (Context.Theory thy)), NONE);
    4.31  
    4.32  fun level state =
    4.33    (case node_of state of
    4.34 @@ -289,22 +288,24 @@
    4.35  
    4.36  local
    4.37  
    4.38 -fun apply_tr _ (Init f) (State ((Toplevel, _), _)) =
    4.39 -      let val node = Theory (Context.Theory (Runtime.controlled_execution NONE f ()))
    4.40 -      in State (node_presentation node, NONE) end
    4.41 -  | apply_tr _ Exit (State ((node as Theory (Context.Theory thy), _), _)) =
    4.42 +fun apply_tr int trans state =
    4.43 +  (case (trans, node_of state) of
    4.44 +    (Init f, Toplevel) =>
    4.45 +      Runtime.controlled_execution NONE (fn () =>
    4.46 +        State (node_presentation (Theory (Context.Theory (f ()))), NONE)) ()
    4.47 +  | (Exit, node as Theory (Context.Theory thy)) =>
    4.48        let
    4.49          val State ((node', pr_ctxt), _) =
    4.50            node |> apply_transaction
    4.51              (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy))))
    4.52              (K ());
    4.53        in State ((Toplevel, pr_ctxt), get_theory node') end
    4.54 -  | apply_tr int (Keep f) state =
    4.55 -      Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
    4.56 -  | apply_tr _ (Transaction _) (State ((Toplevel, _), _)) = raise UNDEF
    4.57 -  | apply_tr int (Transaction (f, g)) (State ((node, _), _)) =
    4.58 -      apply_transaction (fn x => f int x) g node
    4.59 -  | apply_tr _ _ _ = raise UNDEF;
    4.60 +  | (Keep f, node) =>
    4.61 +      Runtime.controlled_execution (try generic_theory_of state)
    4.62 +        (fn () => (f int state; State (node_presentation node, previous_theory_of state))) ()
    4.63 +  | (Transaction _, Toplevel) => raise UNDEF
    4.64 +  | (Transaction (f, g), node) => apply_transaction (fn x => f int x) g node
    4.65 +  | _ => raise UNDEF);
    4.66  
    4.67  fun apply_union _ [] state = raise FAILURE (state, UNDEF)
    4.68    | apply_union int (tr :: trs) state =
    4.69 @@ -314,9 +315,18 @@
    4.70            | exn as FAILURE _ => raise exn
    4.71            | exn => raise FAILURE (state, exn);
    4.72  
    4.73 +fun apply_markers markers (state as State ((node, pr_ctxt), prev_thy)) =
    4.74 +  let
    4.75 +    val state' =
    4.76 +      Runtime.controlled_execution (try generic_theory_of state)
    4.77 +        (fn () => State ((node, fold Document_Marker.evaluate markers pr_ctxt), prev_thy)) ();
    4.78 +  in (state', NONE) end
    4.79 +  handle exn => (state, SOME exn);
    4.80 +
    4.81  in
    4.82  
    4.83 -fun apply_trans int trs state = (apply_union int trs state, NONE)
    4.84 +fun apply_trans int trans markers state =
    4.85 +  (apply_union int trans state |> apply_markers markers)
    4.86    handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
    4.87  
    4.88  end;
    4.89 @@ -325,18 +335,19 @@
    4.90  (* datatype transition *)
    4.91  
    4.92  datatype transition = Transition of
    4.93 - {name: string,              (*command name*)
    4.94 -  pos: Position.T,           (*source position*)
    4.95 -  timing: Time.time,         (*prescient timing information*)
    4.96 -  trans: trans list};        (*primitive transitions (union)*)
    4.97 + {name: string,               (*command name*)
    4.98 +  pos: Position.T,            (*source position*)
    4.99 +  markers: Input.source list, (*semantic document markers*)
   4.100 +  timing: Time.time,          (*prescient timing information*)
   4.101 +  trans: trans list};         (*primitive transitions (union)*)
   4.102  
   4.103 -fun make_transition (name, pos, timing, trans) =
   4.104 -  Transition {name = name, pos = pos, timing = timing, trans = trans};
   4.105 +fun make_transition (name, pos, markers, timing, trans) =
   4.106 +  Transition {name = name, pos = pos, markers = markers, timing = timing, trans = trans};
   4.107  
   4.108 -fun map_transition f (Transition {name, pos, timing, trans}) =
   4.109 -  make_transition (f (name, pos, timing, trans));
   4.110 +fun map_transition f (Transition {name, pos, markers, timing, trans}) =
   4.111 +  make_transition (f (name, pos, markers, timing, trans));
   4.112  
   4.113 -val empty = make_transition ("", Position.none, Time.zeroTime, []);
   4.114 +val empty = make_transition ("", Position.none, [], Time.zeroTime, []);
   4.115  
   4.116  
   4.117  (* diagnostics *)
   4.118 @@ -355,20 +366,23 @@
   4.119  
   4.120  (* modify transitions *)
   4.121  
   4.122 -fun name name = map_transition (fn (_, pos, timing, trans) =>
   4.123 -  (name, pos, timing, trans));
   4.124 +fun name name = map_transition (fn (_, pos, markers, timing, trans) =>
   4.125 +  (name, pos, markers, timing, trans));
   4.126  
   4.127 -fun position pos = map_transition (fn (name, _, timing, trans) =>
   4.128 -  (name, pos, timing, trans));
   4.129 +fun position pos = map_transition (fn (name, _, markers, timing, trans) =>
   4.130 +  (name, pos, markers, timing, trans));
   4.131 +
   4.132 +fun markers markers = map_transition (fn (name, pos, _, timing, trans) =>
   4.133 +  (name, pos, markers, timing, trans));
   4.134  
   4.135 -fun timing timing = map_transition (fn (name, pos, _, trans) =>
   4.136 -  (name, pos, timing, trans));
   4.137 +fun timing timing = map_transition (fn (name, pos, markers, _, trans) =>
   4.138 +  (name, pos, markers, timing, trans));
   4.139  
   4.140 -fun add_trans tr = map_transition (fn (name, pos, timing, trans) =>
   4.141 -  (name, pos, timing, tr :: trans));
   4.142 +fun add_trans tr = map_transition (fn (name, pos, markers, timing, trans) =>
   4.143 +  (name, pos, markers, timing, tr :: trans));
   4.144  
   4.145 -val reset_trans = map_transition (fn (name, pos, timing, _) =>
   4.146 -  (name, pos, timing, []));
   4.147 +val reset_trans = map_transition (fn (name, pos, markers, timing, _) =>
   4.148 +  (name, pos, markers, timing, []));
   4.149  
   4.150  
   4.151  (* basic transitions *)
   4.152 @@ -605,9 +619,9 @@
   4.153  
   4.154  local
   4.155  
   4.156 -fun app int (tr as Transition {trans, ...}) =
   4.157 +fun app int (tr as Transition {markers, trans, ...}) =
   4.158    setmp_thread_position tr
   4.159 -    (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans)
   4.160 +    (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans markers)
   4.161        ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn));
   4.162  
   4.163  in
   4.164 @@ -707,18 +721,26 @@
   4.165          then Future.proofs_enabled 1
   4.166          else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate));
   4.167  
   4.168 +val empty_markers = markers [];
   4.169 +val empty_trans = reset_trans #> keep (K ());
   4.170 +
   4.171 +in
   4.172 +
   4.173 +fun fork_presentation tr = (tr |> empty_markers, tr |> empty_trans);
   4.174 +
   4.175  fun atom_result keywords tr st =
   4.176    let
   4.177      val st' =
   4.178        if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
   4.179 -        (Execution.fork
   4.180 -          {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
   4.181 -          (fn () => command tr st); st)
   4.182 +        let
   4.183 +          val (tr1, tr2) = fork_presentation tr;
   4.184 +          val _ =
   4.185 +            Execution.fork {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
   4.186 +              (fn () => command tr1 st);
   4.187 +        in command tr2 st end
   4.188        else command tr st;
   4.189    in (Result (tr, st'), st') end;
   4.190  
   4.191 -in
   4.192 -
   4.193  fun element_result keywords (Thy_Element.Element (tr, NONE)) st = atom_result keywords tr st
   4.194    | element_result keywords (elem as Thy_Element.Element (head_tr, SOME element_rest)) st =
   4.195        let
   4.196 @@ -734,6 +756,8 @@
   4.197            in (Result_List (head_result :: proof_results), st'') end
   4.198          else
   4.199            let
   4.200 +            val (end_tr1, end_tr2) = fork_presentation end_tr;
   4.201 +
   4.202              val finish = Context.Theory o Proof_Context.theory_of;
   4.203  
   4.204              val future_proof =
   4.205 @@ -744,10 +768,10 @@
   4.206                      let
   4.207                        val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st';
   4.208                        val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy));
   4.209 -                      val (result, result_state) =
   4.210 +                      val (results, result_state) =
   4.211                          State (node_presentation node', prev_thy)
   4.212 -                        |> fold_map (element_result keywords) body_elems ||> command end_tr;
   4.213 -                    in (Result_List result, presentation_context0 result_state) end))
   4.214 +                        |> fold_map (element_result keywords) body_elems ||> command end_tr1;
   4.215 +                    in (Result_List results, presentation_context0 result_state) end))
   4.216                #> (fn (res, state') => state' |> put_result (Result_Future res));
   4.217  
   4.218              val forked_proof =
   4.219 @@ -756,12 +780,12 @@
   4.220                end_proof (fn _ => future_proof #>
   4.221                  (fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
   4.222  
   4.223 -            val st'' = st'
   4.224 -              |> command (head_tr |> reset_trans |> forked_proof);
   4.225 -            val end_result = Result (end_tr, st'');
   4.226 +            val st'' = st' |> command (head_tr |> reset_trans |> forked_proof);
   4.227 +            val end_st = st'' |> command end_tr2;
   4.228 +            val end_result = Result (end_tr, end_st);
   4.229              val result =
   4.230                Result_List [head_result, Result.get (presentation_context0 st''), end_result];
   4.231 -          in (result, st'') end
   4.232 +          in (result, end_st) end
   4.233        end;
   4.234  
   4.235  end;
     5.1 --- a/src/Pure/PIDE/command.ML	Sat Mar 09 23:57:07 2019 +0100
     5.2 +++ b/src/Pure/PIDE/command.ML	Sun Mar 10 00:21:34 2019 +0100
     5.3 @@ -217,8 +217,12 @@
     5.4  
     5.5  fun run keywords int tr st =
     5.6    if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
     5.7 -    (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
     5.8 -      (fn () => Toplevel.command_exception int tr st); ([], SOME st))
     5.9 +    let
    5.10 +      val (tr1, tr2) = Toplevel.fork_presentation tr;
    5.11 +      val _ =
    5.12 +        Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
    5.13 +          (fn () => Toplevel.command_exception int tr1 st);
    5.14 +    in Toplevel.command_errors int tr2 st end
    5.15    else Toplevel.command_errors int tr st;
    5.16  
    5.17  fun check_token_comments ctxt tok =
     6.1 --- a/src/Pure/PIDE/command.scala	Sat Mar 09 23:57:07 2019 +0100
     6.2 +++ b/src/Pure/PIDE/command.scala	Sun Mar 10 00:21:34 2019 +0100
     6.3 @@ -475,6 +475,7 @@
     6.4        toks match {
     6.5          case (t1, i1) :: (t2, i2) :: rest =>
     6.6            if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest)
     6.7 +          else if (t1.is_keyword && Symbol.is_marker(t1.source) && t2.is_embedded) clean(rest)
     6.8            else (t1, i1) :: clean((t2, i2) :: rest)
     6.9          case _ => toks
    6.10        }
     7.1 --- a/src/Pure/PIDE/markup.ML	Sat Mar 09 23:57:07 2019 +0100
     7.2 +++ b/src/Pure/PIDE/markup.ML	Sun Mar 10 00:21:34 2019 +0100
     7.3 @@ -32,6 +32,7 @@
     7.4    val language_ML: bool -> T
     7.5    val language_SML: bool -> T
     7.6    val language_document: bool -> T
     7.7 +  val language_document_marker: T
     7.8    val language_antiquotation: T
     7.9    val language_text: bool -> T
    7.10    val language_verbatim: bool -> T
    7.11 @@ -314,6 +315,8 @@
    7.12  val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
    7.13  val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
    7.14  val language_document = language' {name = "document", symbols = false, antiquotes = true};
    7.15 +val language_document_marker =
    7.16 +  language {name = "document_marker", symbols = true, antiquotes = true, delimited = true};
    7.17  val language_antiquotation =
    7.18    language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
    7.19  val language_text = language' {name = "text", symbols = true, antiquotes = false};
     8.1 --- a/src/Pure/Pure.thy	Sat Mar 09 23:57:07 2019 +0100
     8.2 +++ b/src/Pure/Pure.thy	Sun Mar 10 00:21:34 2019 +0100
     8.3 @@ -7,7 +7,7 @@
     8.4  theory Pure
     8.5  keywords
     8.6      "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
     8.7 -    "\<subseteq>" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
     8.8 +    "\<marker>" "\<subseteq>" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
     8.9      "overloaded" "pervasive" "premises" "structure" "unchecked"
    8.10    and "private" "qualified" :: before_command
    8.11    and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
     9.1 --- a/src/Pure/ROOT.ML	Sat Mar 09 23:57:07 2019 +0100
     9.2 +++ b/src/Pure/ROOT.ML	Sun Mar 10 00:21:34 2019 +0100
     9.3 @@ -208,6 +208,7 @@
     9.4  ML_file "Isar/parse.ML";
     9.5  ML_file "Thy/document_source.ML";
     9.6  ML_file "Thy/thy_header.ML";
     9.7 +ML_file "Thy/document_marker.ML";
     9.8  
     9.9  (*proof context*)
    9.10  ML_file "Isar/object_logic.ML";
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Pure/Thy/document_marker.ML	Sun Mar 10 00:21:34 2019 +0100
    10.3 @@ -0,0 +1,64 @@
    10.4 +(*  Title:      Pure/Thy/document_marker.ML
    10.5 +    Author:     Makarius
    10.6 +
    10.7 +Document markers: declarations on the presentation context.
    10.8 +*)
    10.9 +
   10.10 +signature DOCUMENT_MARKER =
   10.11 +sig
   10.12 +  type marker = Proof.context -> Proof.context
   10.13 +  val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
   10.14 +  val evaluate: Input.source -> marker
   10.15 +end;
   10.16 +
   10.17 +structure Document_Marker: DOCUMENT_MARKER =
   10.18 +struct
   10.19 +
   10.20 +(* theory data *)
   10.21 +
   10.22 +type marker = Proof.context -> Proof.context;
   10.23 +
   10.24 +structure Markers = Theory_Data
   10.25 +(
   10.26 +  type T = (Token.src -> Proof.context -> Proof.context) Name_Space.table;
   10.27 +  val empty : T = Name_Space.empty_table "document_marker";
   10.28 +  val extend = I;
   10.29 +  val merge = Name_Space.merge_tables;
   10.30 +);
   10.31 +
   10.32 +val get_markers = Markers.get o Proof_Context.theory_of;
   10.33 +
   10.34 +fun check ctxt = Name_Space.check (Context.Proof ctxt) (get_markers ctxt);
   10.35 +
   10.36 +fun setup name scan body thy =
   10.37 +  let
   10.38 +    fun marker src ctxt =
   10.39 +      let val (x, ctxt') = Token.syntax scan src ctxt
   10.40 +      in body x ctxt' end;
   10.41 +  in thy |> Markers.map (Name_Space.define (Context.Theory thy) true (name, marker) #> #2) end;
   10.42 +
   10.43 +
   10.44 +(* evaluate inner syntax *)
   10.45 +
   10.46 +val parse_marker = Parse.token Parse.liberal_name ::: Parse.!!! Parse.args;
   10.47 +
   10.48 +fun evaluate input ctxt =
   10.49 +  let
   10.50 +    val pos = Input.pos_of input;
   10.51 +    val _ = Context_Position.report ctxt pos Markup.language_document_marker;
   10.52 +
   10.53 +    val syms = Input.source_explode input;
   10.54 +    val markers =
   10.55 +      (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) syms of
   10.56 +        SOME res => res
   10.57 +      | NONE => error ("Bad input" ^ Position.here pos));
   10.58 +  in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end;
   10.59 +
   10.60 +
   10.61 +(* concrete markers *)
   10.62 +
   10.63 +val _ =
   10.64 +  Theory.setup
   10.65 +    (setup (Binding.make ("tag", \<^here>)) (Scan.lift Parse.name) Document_Source.update_tags);
   10.66 +
   10.67 +end;
    11.1 --- a/src/Pure/Thy/document_source.ML	Sat Mar 09 23:57:07 2019 +0100
    11.2 +++ b/src/Pure/Thy/document_source.ML	Sun Mar 10 00:21:34 2019 +0100
    11.3 @@ -14,8 +14,10 @@
    11.4    val improper: Token.T list parser
    11.5    val improper_end: Token.T list parser
    11.6    val blank_end: Token.T list parser
    11.7 -  val tag: string parser
    11.8 +  val get_tags: Proof.context -> string list
    11.9 +  val update_tags: string -> Proof.context -> Proof.context
   11.10    val tags: string list parser
   11.11 +  val annotation: Input.source list parser
   11.12  end;
   11.13  
   11.14  structure Document_Source: DOCUMENT_SOURCE =
   11.15 @@ -41,11 +43,32 @@
   11.16  val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
   11.17  
   11.18  
   11.19 -(* tags *)
   11.20 +(* syntactic tags (old-style) *)
   11.21 +
   11.22 +structure Tags = Proof_Data
   11.23 +(
   11.24 +  type T = string list;
   11.25 +  fun init _ = [];
   11.26 +);
   11.27 +
   11.28 +val get_tags = Tags.get;
   11.29 +val update_tags = Tags.map o update (op =);
   11.30  
   11.31  val tag_name = Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string);
   11.32  
   11.33  val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (tag_name --| blank_end);
   11.34  val tags = Scan.repeat tag;
   11.35  
   11.36 +
   11.37 +(* semantic markers (operation on presentation context) *)
   11.38 +
   11.39 +val marker =
   11.40 +  (improper -- Parse.$$$ "\<marker>" -- improper) |--
   11.41 +    Parse.!!! (Parse.group (fn () => "document marker") (Parse.input Parse.embedded) --| blank_end);
   11.42 +
   11.43 +val tag_marker =  (*emulation of old-style tags*)
   11.44 +  tag >> (fn name => Input.string ("tag " ^ Symbol_Pos.quote_string_qq name));
   11.45 +
   11.46 +val annotation = Scan.repeat (marker || tag_marker);
   11.47 +
   11.48  end;
    12.1 --- a/src/Pure/Thy/thy_header.ML	Sat Mar 09 23:57:07 2019 +0100
    12.2 +++ b/src/Pure/Thy/thy_header.ML	Sun Mar 10 00:21:34 2019 +0100
    12.3 @@ -175,10 +175,11 @@
    12.4      Parse.command_name textN ||
    12.5      Parse.command_name txtN ||
    12.6      Parse.command_name text_rawN) --
    12.7 -  Document_Source.tags -- Parse.!!! Parse.document_source;
    12.8 +  Document_Source.annotation -- Parse.!!! Parse.document_source;
    12.9  
   12.10  val parse_header =
   12.11 -  (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.tags) |-- Parse.!!! args;
   12.12 +  (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.annotation)
   12.13 +    |-- Parse.!!! args;
   12.14  
   12.15  fun read_tokens pos toks =
   12.16    filter Token.is_proper toks
    13.1 --- a/src/Pure/Thy/thy_header.scala	Sat Mar 09 23:57:07 2019 +0100
    13.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Mar 10 00:21:34 2019 +0100
    13.3 @@ -172,9 +172,9 @@
    13.4            command(TEXT) |
    13.5            command(TXT) |
    13.6            command(TEXT_RAW)) ~
    13.7 -        tags ~! document_source
    13.8 +        annotation ~! document_source
    13.9  
   13.10 -      (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   13.11 +      (rep(heading) ~ command(THEORY) ~ annotation) ~! args ^^ { case _ ~ x => x }
   13.12      }
   13.13    }
   13.14  
    14.1 --- a/src/Pure/Thy/thy_output.ML	Sat Mar 09 23:57:07 2019 +0100
    14.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Mar 10 00:21:34 2019 +0100
    14.3 @@ -202,7 +202,7 @@
    14.4  
    14.5  (* command spans *)
    14.6  
    14.7 -type command = string * Position.T * string list;   (*name, position, tags*)
    14.8 +type command = string * Position.T;   (*name, position*)
    14.9  type source = (token * (string * int)) list;        (*token, markup flag, meta-comment depth*)
   14.10  
   14.11  datatype span = Span of command * (source * source * source * source) * bool;
   14.12 @@ -287,7 +287,8 @@
   14.13          #> cons (Latex.string flag)
   14.14        | _ => I);
   14.15  
   14.16 -    val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
   14.17 +    val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
   14.18 +    val cmd_tags = Document_Source.get_tags (Toplevel.presentation_context state');
   14.19  
   14.20      val (tag, tags) = tag_stack;
   14.21      val {tag', active_tag'} =
   14.22 @@ -371,19 +372,19 @@
   14.23        Document_Source.improper |--
   14.24          Parse.position (Scan.one (fn tok =>
   14.25            Token.is_command tok andalso pred keywords (Token.content_of tok))) --
   14.26 -      Scan.repeat Document_Source.tag --
   14.27 -      Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
   14.28 -        Parse.document_source --| Document_Source.improper_end)
   14.29 -          >> (fn (((tok, pos'), tags), source) =>
   14.30 -            let val name = Token.content_of tok
   14.31 -            in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
   14.32 +      (Document_Source.annotation |--
   14.33 +        Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
   14.34 +          Parse.document_source --| Document_Source.improper_end))
   14.35 +            >> (fn ((tok, pos'), source) =>
   14.36 +              let val name = Token.content_of tok
   14.37 +              in (SOME (name, pos'), (mk (name, source), (flag, d))) end));
   14.38  
   14.39      val command = Scan.peek (fn d =>
   14.40        Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
   14.41 -      Scan.one Token.is_command -- Document_Source.tags
   14.42 -      >> (fn ((cmd_mod, cmd), tags) =>
   14.43 +      Scan.one Token.is_command --| Document_Source.annotation
   14.44 +      >> (fn (cmd_mod, cmd) =>
   14.45          map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
   14.46 -          [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
   14.47 +          [(SOME (Token.content_of cmd, Token.pos_of cmd),
   14.48              (Basic_Token cmd, (markup_false, d)))]));
   14.49  
   14.50      val cmt = Scan.peek (fn d =>