support "tag" marker with scope;

--- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 11 21:33:21 2019 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Apr 12 17:09:21 2019 +0200
@@ -233,7 +233,7 @@
         |> 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 >>
+        Parse.command |-- Document_Source.old_tags >>
           (fn tags => Toplevel.markers (map Document_Marker.legacy_tag tags @ markers) tr0);
     in
       (case lookup_commands thy name of

--- a/src/Pure/Isar/toplevel.ML	Thu Apr 11 21:33:21 2019 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri Apr 12 17:09:21 2019 +0200
@@ -312,18 +312,18 @@
           | exn as FAILURE _ => raise exn
           | exn => raise FAILURE (state, exn);
 
-fun apply_markers markers (state as State ((node, pr_ctxt), prev_thy)) =
+fun apply_markers name 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)) ();
+        (fn () => State ((node, fold (Document_Marker.evaluate name) markers pr_ctxt), prev_thy)) ();
   in (state', NONE) end
   handle exn => (state, SOME exn);
 
 in
 
-fun apply_trans int trans markers state =
-  (apply_union int trans state |> apply_markers markers)
+fun apply_trans int name markers trans state =
+  (apply_union int trans state |> apply_markers name markers)
   handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
 
 end;
@@ -616,9 +616,9 @@
 
 local
 
-fun app int (tr as Transition {markers, trans, ...}) =
+fun app int (tr as Transition {name, markers, trans, ...}) =
   setmp_thread_position tr
-    (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans markers)
+    (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int name markers trans)
       ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn));
 
 in

--- a/src/Pure/Thy/document_marker.ML	Thu Apr 11 21:33:21 2019 +0200
+++ b/src/Pure/Thy/document_marker.ML	Fri Apr 12 17:09:21 2019 +0200
@@ -10,7 +10,8 @@
   val check: Proof.context -> string * Position.T -> string * (Token.src -> marker)
   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 evaluate: string -> Input.source -> marker
+  val command_name: Proof.context -> string
   val legacy_tag: string -> Input.source
 end;
 
@@ -45,9 +46,12 @@
 
 (* evaluate inner syntax *)
 
+val config_command_name = Config.declare_string ("command_name", \<^here>) (K "");
+val command_name = Config.apply config_command_name;
+
 val parse_marker = Parse.token Parse.liberal_name ::: Parse.!!! Parse.args;
 
-fun evaluate input ctxt =
+fun evaluate cmd_name input ctxt =
   let
     val syms = Input.source_explode input
       |> drop_prefix (fn (s, _) => s = Symbol.marker);
@@ -60,7 +64,26 @@
       (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));
-  in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end;
+  in
+    ctxt
+    |> Config.put config_command_name cmd_name
+    |> fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers
+    |> Config.put config_command_name (command_name ctxt)
+  end;
+
+
+(* tag with scope *)
+
+val parse_tag =
+  Scan.state :|-- (fn context =>
+    let
+      val ctxt = Context.proof_of context;
+      val scope0 =
+        if Keyword.is_theory_goal (Thy_Header.get_keywords' ctxt) (command_name ctxt)
+        then Document_Source.Command
+        else Document_Source.Proof;
+      val tag = Scan.optional Document_Source.tag_scope scope0 -- Document_Source.tag_name >> swap;
+    in Scan.lift tag end);
 
 
 (* concrete markers *)
@@ -70,7 +93,7 @@
 
 val _ =
   Theory.setup
-    (setup0 (Binding.make ("tag", \<^here>)) Parse.name Document_Source.update_tags #>
+    (setup (Binding.make ("tag", \<^here>)) parse_tag Document_Source.update_tags #>
      setup0 (Binding.make ("title", \<^here>)) Parse.embedded (meta_data Markup.meta_title) #>
      setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #>
      setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
@@ -84,6 +107,6 @@
         in meta_data Markup.meta_description arg ctxt end));
 
 fun legacy_tag name =
-  Input.string (cartouche ("tag " ^ Symbol_Pos.quote_string_qq name));
+  Input.string (cartouche ("tag (proof) " ^ Symbol_Pos.quote_string_qq name));
 
 end;

--- a/src/Pure/Thy/document_source.ML	Thu Apr 11 21:33:21 2019 +0200
+++ b/src/Pure/Thy/document_source.ML	Fri Apr 12 17:09:21 2019 +0200
@@ -14,9 +14,16 @@
   val improper: Token.T list parser
   val improper_end: Token.T list parser
   val blank_end: Token.T list parser
-  val get_tags: Proof.context -> string list
-  val update_tags: string -> Proof.context -> Proof.context
-  val tags: string list parser
+  datatype scope = Command | Proof
+  type tag = string * scope
+  val eq_tag: tag * tag -> bool
+  val update_tags: tag -> Proof.context -> Proof.context
+  val get_tags: Proof.context -> tag list
+  type tagging = tag list
+  val update_tagging: Proof.context -> tagging -> tag option * tagging
+  val tag_scope: scope parser
+  val tag_name: string parser
+  val old_tags: string list parser
   val annotation: unit parser
 end;
 
@@ -43,27 +50,62 @@
 val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
 
 
-(* syntactic tags (old-style) *)
+(** syntactic tags **)
+
+(* scope *)
+
+datatype scope = Command | Proof;
+
+type tag = string * scope;
+val eq_tag: tag * tag -> bool = eq_fst op =;
+
+
+(* context data *)
 
 structure Tags = Proof_Data
 (
-  type T = string list;
+  type T = tag list;
   fun init _ = [];
 );
 
+val update_tags = Tags.map o update eq_tag;
+
 val get_tags = Tags.get;
-val update_tags = Tags.map o update (op =);
+
+
+(* command tagging *)
+
+type tagging = tag list;
+
+fun update_tagging ctxt tagging =
+  let
+    val tagging' = fold (update eq_tag) (get_tags ctxt) tagging;
+    val nested_tagging' = filter (fn (_, scope) => scope = Proof) tagging';
+  in (try hd tagging', nested_tagging') end;
+
 
-val tag_name = Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string);
+(* parse scope and name *)
+
+val scope = Parse.reserved "command" >> K Command || Parse.reserved "proof" >> K Proof;
+
+val tag_scope =
+  Parse.group (fn () => "document tag scope") (Parse.$$$ "(" |-- Parse.!!! (scope --| Parse.$$$ ")"));
 
-val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (tag_name --| blank_end);
-val tags = Scan.repeat tag;
+val tag_name =
+  Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string);
+
+
+(* syntactic tags (old-style) *)
+
+val old_tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (tag_name --| blank_end);
+
+val old_tags = Scan.repeat old_tag;
 
 
 (* semantic markers (operation on presentation context) *)
 
 val marker = improper |-- Parse.document_marker --| blank_end;
 
-val annotation = Scan.repeat (tag >> K () || marker >> K ()) >> K ();
+val annotation = Scan.repeat (old_tag >> K () || marker >> K ()) >> K ();
 
 end;

--- a/src/Pure/Thy/thy_header.ML	Thu Apr 11 21:33:21 2019 +0200
+++ b/src/Pure/Thy/thy_header.ML	Fri Apr 12 17:09:21 2019 +0200
@@ -137,7 +137,7 @@
 
 val keyword_spec =
   Parse.group (fn () => "outer syntax keyword specification")
-    (Parse.name -- opt_files -- Document_Source.tags);
+    (Parse.name -- opt_files -- Document_Source.old_tags);
 
 val keyword_decl =
   Scan.repeat1 Parse.string_position --

--- a/src/Pure/Thy/thy_output.ML	Thu Apr 11 21:33:21 2019 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Apr 12 17:09:21 2019 +0200
@@ -240,21 +240,22 @@
 fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
 fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
 
-fun document_tag cmd_pos state state' tag_stack =
+fun document_tag cmd_pos state state' tagging_stack =
   let
     val ctxt' = Toplevel.presentation_context state';
     val nesting = Toplevel.level state' - Toplevel.level state;
 
-    val (tag, tags) = tag_stack;
-    val tag' = try hd (fold (update (op =)) (Document_Source.get_tags ctxt') (the_list tag));
-    val tag_stack' =
-      if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
-      else if nesting >= 0 then (tag', replicate nesting tag @ tags)
+    val (tagging, taggings) = tagging_stack;
+    val (tag', tagging') = Document_Source.update_tagging ctxt' tagging;
+
+    val tagging_stack' =
+      if nesting = 0 andalso not (Toplevel.is_proof state) then tagging_stack
+      else if nesting >= 0 then (tagging', replicate nesting tagging @ taggings)
       else
-        (case drop (~ nesting - 1) tags of
+        (case drop (~ nesting - 1) taggings of
           tg :: tgs => (tg, tgs)
         | [] => err_bad_nesting (Position.here cmd_pos));
-  in (tag', tag_stack') end;
+  in (tag', tagging_stack') end;
 
 fun read_tag s =
   (case space_explode "%" s of
@@ -290,7 +291,7 @@
   end;
 
 fun present_span command_tag span state state'
-    (tag_stack, active_tag, newline, latex, present_cont) =
+    (tagging_stack, active_tag, newline, latex, present_cont) =
   let
     val ctxt' = Toplevel.presentation_context state';
     val present = fold (fn (tok, (flag, 0)) =>
@@ -300,8 +301,10 @@
 
     val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
 
-    val (tag', tag_stack') = document_tag cmd_pos state state' tag_stack;
-    val active_tag' = if is_some tag' then tag' else command_tag cmd_name state state' active_tag;
+    val (tag', tagging_stack') = document_tag cmd_pos state state' tagging_stack;
+    val active_tag' =
+      if is_some tag' then Option.map #1 tag'
+      else command_tag cmd_name state state' active_tag;
     val edge = (active_tag, active_tag');
 
     val newline' =
@@ -318,7 +321,7 @@
     val present_cont' =
       if newline then (present (#3 srcs), present (#4 srcs))
       else (I, present (#3 srcs) #> present (#4 srcs));
-  in (tag_stack', active_tag', newline', latex', present_cont') end;
+  in (tagging_stack', active_tag', newline', latex', present_cont') end;
 
 fun present_trailer ((_, tags), active_tag, _, latex, present_cont) =
   if not (null tags) then err_bad_nesting " at end of theory"
@@ -447,7 +450,7 @@
       | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
   in
     if length command_results = length spans then
-      ((NONE, []), NONE, true, [], (I, I))
+      (([], []), NONE, true, [], (I, I))
       |> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
       |> present_trailer
       |> rev