Merge branch 'master' into Unreleased/Isabelle2018

.ci/Jenkinsfile

@@ -5,22 +5,22 @@ pipeline {
         stage('Build Docker') {
             steps {
                 sh 'cp src/patches/thy_output.ML .ci/isabelle4isadof/'
-                sh 'docker build -t logicalhacking:isabelle4dof .ci/isabelle4isadof'
+                sh 'docker build -t logicalhacking:isabelle4dof-2018 .ci/isabelle4isadof'
                 sh 'rm -f .ci/isabelle4isadof/thy_output.ML'
             }
         }
         stage('Check Docker') {
             when { changeset "src/patches/*" } 
             steps {
-                sh 'cp src/patches/thy_output.ML .ci/isabelle4isadof/'
-                sh 'docker build --no-cache -t logicalhacking:isabelle4dof .ci/isabelle4isadof'
+                sh 'cp patches/thy_output.ML .ci/isabelle4isadof/'
+                sh 'docker build --no-cache -t logicalhacking:isabelle4dof-2018 .ci/isabelle4isadof'
                 sh 'rm -f .ci/isabelle4isadof/thy_output.ML'
             }
         }
         stage('Build Isabelle/DOF') {
             steps {
                 sh 'find -type d -name "output" -exec rm -rf {} \\; || true'
-                sh 'docker run -v $PWD:/DOF logicalhacking:isabelle4dof  sh -c "cd /DOF && ./install && isabelle build -D ."'
+                sh 'docker run -v $PWD:/DOF logicalhacking:isabelle4dof-2018  sh -c "cd /DOF && ./install && isabelle build -D ."'
             } 
 	}
     }

.ci/isabelle4isadof/Dockerfile

@@ -24,7 +24,7 @@
 #
 # SPDX-License-Identifier: BSD-2-Clause
 
-FROM logicalhacking:isabelle2019
+FROM logicalhacking:isabelle2018
 
 WORKDIR /home/isabelle
 COPY thy_output.ML /home/isabelle/Isabelle/src/Pure/Thy

.config

@@ -1,8 +1,8 @@
 DOF_VERSION="Unreleased"
-ISABELLE_VERSION="Isabelle2019: June 2019"
-ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2019/"
+ISABELLE_VERSION="Isabelle2018: August 2018"
+ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2018/"
 DOF_URL="https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
 DOF_ARTIFACT_DIR="releases/Isabelle_DOF/Isabelle_DOF"
 DOF_ARTIFACT_HOST="artifacts.logicalhacking.com"
-AFP_DATE="afp-2019-06-17"
-AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
+AFP_DATE="afp-2019-06-04"
+AFP_URL="https://sourceforge.net/projects/afp/files/afp-Isabelle2018/"$AFP_DATE".tar.gz"

README.md

@@ -8,9 +8,9 @@ development.
 
 Isabelle/DOF has two major pre-requisites:
 
-* **Isabelle:** Isabelle/DOF requires [Isabelle 2019](http://isabelle.in.tum.de/website-Isabelle2019/).
-  Please download the Isabelle 2019 distribution for your operating
-  system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2019/).
+* **Isabelle:** Isabelle/DOF requires [Isabelle 2018](http://isabelle.in.tum.de/website-Isabelle2018/).
+  Please download the Isabelle 2018 distribution for your operating
+  system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2018/).
 * **LaTeX:** Isabelle/DOF requires a modern pdfTeX-engine supporting the \expanded{}-primitive. This
   is, for example, included in the [TeXLive 2019](https://www.tug.org/texlive/) (or later)
   distribution. Please follow the [TeXLive installation instructions](https://www.tug.org/texlive/acquire-netinstall.html)
@@ -29,7 +29,7 @@ one), the full path to the ``isabelle`` command needs to be passed as
 using the ``--isabelle`` command line argument of the ``install`` script:
 
 ```console
-foo@bar:~$ ./install --isabelle /usr/local/Isabelle2019/bin/isabelle
+foo@bar:~$ ./install --isabelle /usr/local/Isabelle2018/bin/isabelle
 ```
 
 For further command line options of the installer, please use the

src/DOF/Isa_DOF.thy

@@ -39,7 +39,7 @@ theory Isa_DOF                (* Isabelle Document Ontology Framework *)
            "lemma*" "theorem*" (* -- intended replacement of Isar std commands.*) 
            "assert*"  ::thy_decl
 
-  and      "print_doc_classes" "print_doc_items" "check_doc_global" :: diag
+  and      "print_doc_classes" "print_doc_items" "gen_sty_template"  "check_doc_global" :: diag
            
   
 begin
@@ -627,6 +627,82 @@ val _ =
   Outer_Syntax.command \<^command_keyword>\<open>check_doc_global\<close> "check global document consistency"
     (Parse.opt_bang >> (fn b => Toplevel.keep (check_doc_global b o Toplevel.context_of)));
 
+
+
+fun write_ontology_latex_sty_template thy = 
+    let 
+        (* 
+        val raw_name = Context.theory_long_name thy
+
+        val curr_thy_name = if String.isPrefix "Draft." raw_name 
+                   then String.substring(raw_name, 6, (String.size raw_name)-6)
+                   else error "Not in ontology definition context"
+        *)
+        val curr_thy_name = Context.theory_name thy
+        val {docobj_tab={tab = x, ...},docclass_tab,...}= get_data_global thy;
+
+        fun toStringLaTeXNewKeyCommand env long_name =
+            "\\expandafter\\newkeycommand\\csname"^" "^"isaDof."^env^"."^long_name^"\\endcsname%\n" 
+        
+        fun toStringMetaArgs true attr_long_names = 
+               enclose "[" "][1]" (commas ("label=,type=%\n" :: attr_long_names))
+           |toStringMetaArgs false attr_long_names = 
+               enclose "[" "][1]" (commas attr_long_names) 
+        
+        fun toStringDocItemBody env =
+            enclose "{%\n\\isamarkupfalse\\isamarkup" 
+                    "{#1}\\label{\\commandkey{label}}\\isamarkuptrue%\n}\n"
+                    env
+                    
+        fun toStringDocItemCommand env long_name attr_long_names = 
+            toStringLaTeXNewKeyCommand env long_name ^
+            toStringMetaArgs true attr_long_names ^
+            toStringDocItemBody env ^"\n"
+        
+        fun toStringDocItemLabel long_name attr_long_names = 
+            toStringLaTeXNewKeyCommand "Label" long_name ^
+            toStringMetaArgs false attr_long_names ^
+            "{%\n\\autoref{#1}\n}\n"
+        
+        fun toStringDocItemRef long_name label attr_long_namesNvalues = 
+            "\\isaDof.Label." ^ long_name ^
+            enclose "[" "]" (commas attr_long_namesNvalues) ^
+            enclose "{" "}" label
+        
+        fun write_file thy filename content =
+            let 
+               val filename = Path.explode filename
+               val master_dir = Resources.master_directory thy
+               val abs_filename = if (Path.is_absolute filename) 
+                                  then filename 
+                                  else Path.append master_dir filename
+            in
+              File.write (abs_filename) content
+              handle (IO.Io{name=name,...}) 
+                     => warning ("Could not write \""^(name)^"\".")
+            end
+
+        fun  write_attr (n, ty, _) = YXML.content_of(Binding.print n)^ "=\n"
+
+        fun write_class (n, {attribute_decl,id,inherits_from,name,params,thy_name,rex,rejectS}) =
+            if curr_thy_name = thy_name then
+                   toStringDocItemCommand "section" n (map write_attr attribute_decl) ^
+                   toStringDocItemCommand "text" n (map write_attr attribute_decl) ^
+                   toStringDocItemLabel n (map write_attr attribute_decl)
+                   (* or parameterising with "env" ? ? ?*)
+            else ""
+        val content = String.concat(map write_class (Symtab.dest docclass_tab))
+        (* val _ = writeln content  -- for interactive testing only, breaks LaTeX compilation *) 
+    in 
+        warning("LaTeX Style file  generation not supported.")
+        (*  write_file thy ("Isa-DOF."^curr_thy_name^".template.sty") content *)
+    end
+
+
+val _ =
+  Outer_Syntax.command \<^command_keyword>\<open>gen_sty_template\<close> "generate a  LaTeX style template"
+    (Parse.opt_bang>>(fn b => Toplevel.keep(write_ontology_latex_sty_template o Toplevel.theory_of)));
+
 val (strict_monitor_checking, strict_monitor_checking_setup) 
      = Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false);
 
@@ -648,7 +724,7 @@ typedecl "thm"
 typedecl "file"
 typedecl "thy"
  
-\<comment> \<open>and others in the future : file, http, thy, ...\<close> 
+\<comment> \<open> and others in the future : file, http, thy, ... \<close> 
 
 consts ISA_typ          :: "string \<Rightarrow> typ"               ("@{typ _}")
 consts ISA_term         :: "string \<Rightarrow> term"              ("@{term _}")
@@ -661,6 +737,8 @@ consts ISA_docitem_attr :: "string \<Rightarrow> string \<Rightarrow> 'a"      (
 
 \<comment> \<open>Dynamic setup of inner syntax cartouche\<close>
 
+
+(* PORT TO ISABELLE2018 *)
 ML \<open>
 (*  Author:     Frédéric Tuong, Université Paris-Saclay *)
 (*  Title:      HOL/ex/Cartouche_Examples.thy
@@ -1411,8 +1489,7 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse
             in ltx end 
 
 
-        fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) 
-                                            (Symbol.explode (YXML.content_of s)))
+        fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) (Symbol.explode (YXML.content_of s)))
         fun ltx_of_markup ctxt s = let
   	                            val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s
                                 val str_of_term = ltx_of_term  ctxt true term 
@@ -1425,8 +1502,7 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse
         val ctxt = Proof_Context.init_global thy
         val actual_args =  map (fn ((lhs,_),rhs) => (toLong lhs, ltx_of_markup ctxt rhs))
                                attr_list  
-	      val default_args = map (fn (b,_,t) => (toLong (Long_Name.base_name ( Sign.full_name thy b)), 
-                                                       ltx_of_term ctxt true t))
+	      val default_args = map (fn (b,_,t) => (toLong (Long_Name.base_name ( Sign.full_name thy b)), ltx_of_term ctxt true t))
                                (DOF_core.get_attribute_defaults cid_long thy)
 
         val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a) 
@@ -1441,7 +1517,7 @@ end
 (* the following 2 lines set parser and converter for LaTeX generation of meta-attributes. 
    Currently of *all* commands, no distinction between text* and text command. 
    This code depends on a MODIFIED Isabelle2017 version resulting from applying the files
-   under src/patches. 
+   under Isabell_DOF/patches. 
  *)
 (* REMARK PORT 2018 : transmission of meta-args to LaTeX crude and untested. Can be found in
    present_token. *)
@@ -1449,13 +1525,14 @@ end
 
 end
 \<close>
-ML\<open> (* Setting in thy_output.ML a parser for the syntactic handling of the meta-informations of 
-       text elements - so text*[m<meta-info>]\<open> ... dfgdfg .... \<close> *)
-                 
+ML\<open>                    
 val _ = Thy_Output.set_meta_args_parser
-            (fn thy => (Scan.optional (Document_Source.improper 
-                                       |--   ODL_Command_Parser.attributes 
-                                       >>    ODL_LTX_Converter.meta_args_2_string thy) "")); \<close>
+                       (fn thy => let val _ = writeln "META_ARGS_PARSING"
+                                  in  (Scan.optional (   ODL_Command_Parser.attributes 
+                                                      >> ODL_LTX_Converter.meta_args_2_string thy) "")
+                                  end); 
+
+\<close>
 
 
 
@@ -1545,9 +1622,9 @@ fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name  =
          in () end
     else if   DOF_core.is_declared_oid_global name thy 
          then (if #strict_checking str 
-               then warning("declared but undefined document reference: "^name) (* HACK bu 29/6.19 *)
+               then warning("declared but undefined document reference:"^name)
                else ())
-         else error("undefined document reference: "^name)
+         else error("undefined document reference:"^name)
   end
 
 val _ =  check_and_mark : Proof.context ->  string ->  {strict_checking: bool} ->
@@ -1572,13 +1649,13 @@ val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input)
 
 fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define = y}, src ) = 
             let (* val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::2::" ^ cid_decl) *)
-                val (str,pos) = Input.source_content src
-                val _ = check_and_mark ctxt cid_decl
-                          ({strict_checking = not x}) pos str 
+                val _ = check_and_mark ctxt cid_decl  
+                          ({strict_checking = not x}) 
+                          (Input.pos_of src) (Input.source_content src) 
             in  
-                (if y  then Latex.enclose_block ("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}]{") "}" 
-                       else Latex.enclose_block ("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}]{") "}")
-                [Latex.text (Input.source_content src)] 
+                (if y  then Latex.enclose_block ("\\csname isadof.label[type={"^cid_decl^"}]{") "}\\endcsname" 
+                       else Latex.enclose_block ("\\csname isadof.ref[type={"^cid_decl^"}]{") "}\\endcsname")
+                [Latex.string (Input.source_content src)] 
             end
           
 
@@ -1606,7 +1683,7 @@ fun check_and_mark_term ctxt oid  =
 fun ML_antiquotation_docitem_value (ctxt, toks) = 
               (Scan.lift (Args.cartouche_input) 
                >> (fn inp => (ML_Syntax.atomic o ML_Syntax.print_term) 
-                             ((check_and_mark_term ctxt o fst o Input.source_content) inp)))
+                             ((check_and_mark_term ctxt o Input.source_content) inp)))
                (ctxt, toks)
 
 (* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*)

src/DOF/RegExpChecker.sml

@@ -276,36 +276,27 @@ val example_expression : nat rexp =
     Times (Star (Plus (Times (r1, r1), r0)), Star (Plus (Times (r0, r0), r1)))
   end;
 
+fun sgn_integer k =
+  (if ((k : IntInf.int) = (0 : IntInf.int)) then (0 : IntInf.int)
+    else (if IntInf.< (k, (0 : IntInf.int)) then (~1 : IntInf.int)
+           else (1 : IntInf.int)));
+
 fun divmod_integer k l =
   (if ((k : IntInf.int) = (0 : IntInf.int))
     then ((0 : IntInf.int), (0 : IntInf.int))
-    else (if IntInf.< ((0 : IntInf.int), l)
-           then (if IntInf.< ((0 : IntInf.int), k)
-                  then IntInf.divMod (IntInf.abs k, IntInf.abs l)
-                  else let
-                         val (r, s) =
-                           IntInf.divMod (IntInf.abs k, IntInf.abs l);
-                       in
-                         (if ((s : IntInf.int) = (0 : IntInf.int))
-                           then (IntInf.~ r, (0 : IntInf.int))
-                           else (IntInf.- (IntInf.~ r, (1 : IntInf.int)),
-                                  IntInf.- (l, s)))
-                       end)
-           else (if ((l : IntInf.int) = (0 : IntInf.int))
-                  then ((0 : IntInf.int), k)
-                  else apsnd IntInf.~
-                         (if IntInf.< (k, (0 : IntInf.int))
-                           then IntInf.divMod (IntInf.abs k, IntInf.abs l)
-                           else let
-                                  val (r, s) =
-                                    IntInf.divMod (IntInf.abs k, IntInf.abs l);
-                                in
-                                  (if ((s : IntInf.int) = (0 : IntInf.int))
-                                    then (IntInf.~ r, (0 : IntInf.int))
-                                    else (IntInf.- (IntInf.~
-              r, (1 : IntInf.int)),
-   IntInf.- (IntInf.~ l, s)))
-                                end))));
+    else (if ((l : IntInf.int) = (0 : IntInf.int)) then ((0 : IntInf.int), k)
+           else (apsnd o (fn a => fn b => IntInf.* (a, b)) o sgn_integer) l
+                  (if (((sgn_integer k) : IntInf.int) = (sgn_integer l))
+                    then IntInf.divMod (IntInf.abs k, IntInf.abs l)
+                    else let
+                           val (r, s) =
+                             IntInf.divMod (IntInf.abs k, IntInf.abs l);
+                         in
+                           (if ((s : IntInf.int) = (0 : IntInf.int))
+                             then (IntInf.~ r, (0 : IntInf.int))
+                             else (IntInf.- (IntInf.~ r, (1 : IntInf.int)),
+                                    IntInf.- (IntInf.abs l, s)))
+                         end)));
 
 fun nat_of_integer k =
   (if IntInf.<= (k, (0 : IntInf.int)) then Zero_nat

src/patches/thy_output.ML

@@ -21,28 +21,19 @@ sig
   val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
   val typewriter: Proof.context -> string -> Latex.text
   val verbatim: Proof.context -> string -> Latex.text
-  val source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text
+  val source: Proof.context -> Token.src -> Latex.text
   val pretty: Proof.context -> Pretty.T -> Latex.text
-  val pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text
+  val pretty_source: Proof.context -> Token.src -> Pretty.T -> Latex.text
   val pretty_items: Proof.context -> Pretty.T list -> Latex.text
-  val pretty_items_source: Proof.context -> {embedded: bool} -> Token.src ->
-    Pretty.T list -> Latex.text
+  val pretty_items_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
   val antiquotation_pretty:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
-  val antiquotation_pretty_embedded:
-    binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_pretty_source:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
-  val antiquotation_pretty_source_embedded:
-    binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_raw:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
-  val antiquotation_raw_embedded:
-    binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
   val antiquotation_verbatim:
     binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
-  val antiquotation_verbatim_embedded:
-    binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
 end;
 
 structure Thy_Output: THY_OUTPUT =
@@ -63,8 +54,8 @@ fun output_comment ctxt (kind, syms) =
       Symbol_Pos.cartouche_content syms
       |> output_symbols
       |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
-  | Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)]
-  | Comment.Marker => [])
+  | Comment.Latex =>
+      [Latex.symbols (Symbol_Pos.cartouche_content syms)])
 and output_comment_document ctxt (comment, syms) =
   (case comment of
     SOME kind => output_comment ctxt (kind, syms)
@@ -141,7 +132,6 @@ fun output_token ctxt tok =
   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)
@@ -163,7 +153,7 @@ fun check_comments ctxt =
       val pos = #1 (Symbol_Pos.range syms);
       val _ =
         comment |> Option.app (fn kind =>
-          Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.kind_markups kind)));
+          Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind)));
       val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
     in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
 
@@ -173,6 +163,15 @@ end;
 
 (** present theory source **)
 
+(*NB: arranging white space around command spans is a black art*)
+
+val is_white = Token.is_space orf Token.is_informal_comment;
+val is_black = not o is_white;
+
+val is_white_comment = Token.is_informal_comment;
+val is_black_comment = Token.is_formal_comment;
+
+
 (* presentation tokens *)
 
 datatype token =
@@ -185,8 +184,8 @@ datatype token =
 fun basic_token pred (Basic_Token tok) = pred tok
   | basic_token _ _ = false;
 
-val white_token = basic_token Document_Source.is_white;
-val white_comment_token = basic_token Document_Source.is_white_comment;
+val white_token = basic_token is_white;
+val white_comment_token = basic_token is_white_comment;
 val blank_token = basic_token Token.is_blank;
 val newline_token = basic_token Token.is_newline;
 
@@ -200,14 +199,14 @@ fun present_token ctxt tok =
   | Markup_Env_Token (cmd, meta_args, source) =>
       [Latex.environment_block
          ("isamarkup" ^ cmd (* ^ meta_args*))
-         (Latex.string meta_args :: output_document ctxt {markdown = true} source)]      
+         (Latex.string meta_args :: output_document ctxt {markdown = true} source)]
   | Raw_Token source =>
       Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
 
 
 (* command spans *)
 
-type command = string * Position.T;   (*name, position*)
+type command = string * Position.T * string list;   (*name, position, tags*)
 type source = (token * (string * int)) list;        (*token, markup flag, meta-comment depth*)
 
 datatype span = Span of command * (source * source * source * source) * bool;
@@ -231,8 +230,8 @@ fun make_span cmd src =
 
 local
 
-fun err_bad_nesting here =
-  error ("Bad nesting of commands in presentation" ^ here);
+fun err_bad_nesting pos =
+  error ("Bad nesting of commands in presentation" ^ pos);
 
 fun edge which f (x: string option, y) =
   if x = y then I
@@ -243,23 +242,6 @@ val end_tag = edge #1 Latex.end_tag;
 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' tagging_stack =
-  let
-    val ctxt' = Toplevel.presentation_context state';
-    val nesting = Toplevel.level state' - Toplevel.level state;
-
-    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) taggings of
-          tg :: tgs => (tg, tgs)
-        | [] => err_bad_nesting (Position.here cmd_pos));
-  in (tag', tagging_stack') end;
-
 fun read_tag s =
   (case space_explode "%" s of
     ["", b] => (SOME b, NONE)
@@ -275,44 +257,61 @@ fun make_command_tag options keywords =
     val document_tags_default = map_filter #1 document_tags;
     val document_tags_command = map_filter #2 document_tags;
   in
-    fn cmd_name => fn state => fn state' => fn active_tag =>
+    fn {cmd_name, cmd_tags, tag, active_tag} => fn state => fn state' =>
       let
+        val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
+
         val keyword_tags =
           if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"]
           else Keyword.command_tags keywords cmd_name;
         val command_tags =
           the_list (AList.lookup (op =) document_tags_command cmd_name) @
           keyword_tags @ document_tags_default;
+
         val active_tag' =
-          (case command_tags of
-            default_tag :: _ => SOME default_tag
-          | [] =>
-              if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
-              then active_tag
-              else NONE);
-      in active_tag' end
+          if is_some tag' then tag'
+          else
+            (case command_tags of
+              default_tag :: _ => SOME default_tag
+            | [] =>
+                if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
+                then active_tag
+                else NONE);
+      in {tag' = tag', active_tag' = active_tag'} end
   end;
 
-fun present_span command_tag span state state'
-    (tagging_stack, active_tag, newline, latex, present_cont) =
+fun present_span thy command_tag span state state'
+    (tag_stack, active_tag, newline, latex, present_cont) =
   let
-    val ctxt' = Toplevel.presentation_context state';
+    val ctxt' =
+      Toplevel.presentation_context state'
+        handle Toplevel.UNDEF => Proof_Context.get_global thy Context.PureN;
     val present = fold (fn (tok, (flag, 0)) =>
         fold cons (present_token ctxt' tok)
         #> cons (Latex.string flag)
       | _ => I);
 
-    val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
+    val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
 
-    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 (tag, tags) = tag_stack;
+    val {tag', active_tag'} =
+      command_tag {cmd_name = cmd_name, cmd_tags = cmd_tags, tag = tag, active_tag = active_tag}
+        state state';
     val edge = (active_tag, active_tag');
 
+    val nesting = Toplevel.level state' - Toplevel.level state;
+
     val newline' =
       if is_none active_tag' then span_newline else newline;
 
+    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)
+      else
+        (case drop (~ nesting - 1) tags of
+          tg :: tgs => (tg, tgs)
+        | [] => err_bad_nesting (Position.here cmd_pos));
+
     val latex' =
       latex
       |> end_tag edge
@@ -324,7 +323,7 @@ fun present_span command_tag span state state'
     val present_cont' =
       if newline then (present (#3 srcs), present (#4 srcs))
       else (I, present (#3 srcs) #> present (#4 srcs));
-  in (tagging_stack', active_tag', newline', latex', present_cont') end;
+  in (tag_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"
@@ -344,6 +343,14 @@ local
 val markup_true = "\\isamarkuptrue%\n";
 val markup_false = "\\isamarkupfalse%\n";
 
+val space_proper =
+  Scan.one Token.is_blank -- Scan.many is_white_comment -- Scan.one is_black;
+
+val is_improper = not o (is_black orf Token.is_begin_ignore orf Token.is_end_ignore);
+val improper = Scan.many is_improper;
+val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
+val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
+
 val opt_newline = Scan.option (Scan.one Token.is_newline);
 
 val ignore =
@@ -353,16 +360,19 @@ val ignore =
     (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
     >> pair (d - 1));
 
+val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
+
 val locale =
-  Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |--
-    Parse.!!!
-      (Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")")));
+  Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
+    Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
 
 (*
 val meta_args_parser_hook =  Synchronized.var "meta args parser hook" 
                              ((fn thy => fn s => ("",s)): theory -> string parser);
 *)
-val meta_args_parser_hook =  Unsynchronized.ref ((fn _ => fn s => ("",s)): theory -> string parser);
+val meta_args_parser_hook =  Unsynchronized.ref 
+                             ((fn thy => fn s => ("",s)): theory -> string parser);
+
 
 in
 
@@ -370,6 +380,7 @@ type segment = {span: Command_Span.span, command: Toplevel.transition, state: To
 
 fun present_thy options thy (segments: segment list) =
   let
+
     val keywords = Thy_Header.get_keywords thy;
 
 
@@ -379,32 +390,30 @@ fun present_thy options thy (segments: segment list) =
       >> (fn d => (NONE, (Ignore_Token, ("", d))));
 
     fun markup pred mk flag = Scan.peek (fn d =>
-      Document_Source.improper 
-      |-- Parse.position (Scan.one (fn tok => Token.is_command tok andalso 
-                                              pred keywords (Token.content_of tok))) 
-      --   (Document_Source.annotation |--
-            (Parse.!!!!
-              (   ( (!meta_args_parser_hook thy))
-               -- ( (Document_Source.improper -- locale -- Document_Source.improper) 
-                    |-- Parse.document_source )
-                     --| Document_Source.improper_end)
-              )
-        
-           )
-        >> (fn ((tok, pos'), (meta_args, source)) =>
-           let val name = Token.content_of tok
-           in (SOME (name, pos'), (mk (name,  meta_args , source), (flag, d))) end));
+      improper |--
+        Parse.position (Scan.one (fn tok =>
+          Token.is_command tok andalso pred keywords (Token.content_of tok))) --
+      Scan.repeat tag --
+      (improper |--
+      (Parse.!!!! 
+      (  (!meta_args_parser_hook thy)
+         -- (  (improper -- locale -- improper) 
+         |-- (Parse.document_source)) 
+         --| improper_end)))
+      >> (fn (((tok, pos'), tags), (meta_args, source)) =>
+        let val name = Token.content_of tok
+        in (SOME (name, pos', tags), (mk (name, meta_args, 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.annotation
-      >> (fn (cmd_mod, cmd) =>
+      Scan.optional (Scan.one Token.is_command_modifier ::: improper) [] --
+      Scan.one Token.is_command -- Scan.repeat tag
+      >> (fn ((cmd_mod, cmd), tags) =>
         map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
-          [(SOME (Token.content_of cmd, Token.pos_of cmd),
+          [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
             (Basic_Token cmd, (markup_false, d)))]));
 
     val cmt = Scan.peek (fn d =>
-      Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
+      Scan.one is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
 
     val other = Scan.peek (fn d =>
        Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
@@ -459,25 +468,28 @@ fun present_thy options thy (segments: segment list) =
     val command_tag = make_command_tag options keywords;
 
     fun present_command tr span st st' =
-      Toplevel.setmp_thread_position tr (present_span command_tag span st st');
+      Toplevel.setmp_thread_position tr (present_span thy command_tag span st st');
 
     fun present _ [] = I
-      | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
+      | present st ((span, (tr, st')) :: rest) = present_command tr span st st' 
+                                                 #> present st' rest;
+
   in
     if length command_results = length spans then
-      (([], []), NONE, true, [], (I, I))
-      |> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
+      ((NONE, []), NONE, true, [], (I, I))
+      |> present Toplevel.toplevel (spans ~~ command_results)
       |> present_trailer
       |> rev
     else error "Messed-up outer syntax for presentation"
   end;
 
-  fun set_meta_args_parser f = 
-    let
-      val _ = writeln "Meta-args parser set to new value"                          
-    in  
-      (meta_args_parser_hook := f)
-    end
+(*
+fun set_meta_args_parser f = let val _ = writeln "Meta-args parser set to new value" 
+                             in  (Unsynchronized.assign meta_args_parser_hook  f) end
+*)
+fun set_meta_args_parser f = let val _ = writeln "Meta-args parser set to new value" 
+                             in  ( meta_args_parser_hook := f) end
+
 
 end;
 
@@ -516,19 +528,9 @@ fun verbatim ctxt =
   then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
   else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
 
-fun token_source ctxt {embedded} tok =
-  if Token.is_kind Token.Cartouche tok andalso embedded andalso
-    not (Config.get ctxt Document_Antiquotation.thy_output_source_cartouche)
-  then Token.content_of tok
-  else Token.unparse tok;
-
-fun is_source ctxt =
-  Config.get ctxt Document_Antiquotation.thy_output_source orelse
-  Config.get ctxt Document_Antiquotation.thy_output_source_cartouche;
-
-fun source ctxt embedded =
+fun source ctxt =
   Token.args_of_src
-  #> map (token_source ctxt embedded #> Document_Antiquotation.prepare_lines ctxt)
+  #> map (Token.unparse #> Document_Antiquotation.prepare_lines ctxt)
   #> space_implode " "
   #> output_source ctxt
   #> isabelle ctxt;
@@ -536,53 +538,33 @@ fun source ctxt embedded =
 fun pretty ctxt =
   Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt;
 
-fun pretty_source ctxt embedded src prt =
-  if is_source ctxt then source ctxt embedded src else pretty ctxt prt;
+fun pretty_source ctxt src prt =
+  if Config.get ctxt Document_Antiquotation.thy_output_source
+  then source ctxt src else pretty ctxt prt;
 
 fun pretty_items ctxt =
   map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt;
 
-fun pretty_items_source ctxt embedded src prts =
-  if is_source ctxt then source ctxt embedded src else pretty_items ctxt prts;
+fun pretty_items_source ctxt src prts =
+  if Config.get ctxt Document_Antiquotation.thy_output_source
+  then source ctxt src else pretty_items ctxt prts;
 
 
 (* antiquotation variants *)
 
-local
+fun antiquotation_pretty name scan f =
+  Document_Antiquotation.setup name scan
+    (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
 
-fun gen_setup name embedded =
-  if embedded
-  then Document_Antiquotation.setup_embedded name
-  else Document_Antiquotation.setup name;
+fun antiquotation_pretty_source name scan f =
+  Document_Antiquotation.setup name scan
+    (fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x));
 
-fun gen_antiquotation_pretty name embedded scan f =
-  gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
+fun antiquotation_raw name scan f =
+  Document_Antiquotation.setup name scan
+    (fn {context = ctxt, argument = x, ...} => f ctxt x);
 
-fun gen_antiquotation_pretty_source name embedded scan f =
-  gen_setup name embedded scan
-    (fn {context = ctxt, source = src, argument = x} =>
-      pretty_source ctxt {embedded = embedded} src (f ctxt x));
-
-fun gen_antiquotation_raw name embedded scan f =
-  gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);
-
-fun gen_antiquotation_verbatim name embedded scan f =
-  gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt);
-
-in
-
-fun antiquotation_pretty name = gen_antiquotation_pretty name false;
-fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true;
-
-fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false;
-fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true;
-
-fun antiquotation_raw name = gen_antiquotation_raw name false;
-fun antiquotation_raw_embedded name = gen_antiquotation_raw name true;
-
-fun antiquotation_verbatim name = gen_antiquotation_verbatim name false;
-fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true;
-
-end;
+fun antiquotation_verbatim name scan f =
+  antiquotation_raw name scan (fn ctxt => verbatim ctxt o f ctxt);
 
 end;

src/patches/thy_output.orig18.ML

@@ -20,28 +20,19 @@ sig
   val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
   val typewriter: Proof.context -> string -> Latex.text
   val verbatim: Proof.context -> string -> Latex.text
-  val source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text
+  val source: Proof.context -> Token.src -> Latex.text
   val pretty: Proof.context -> Pretty.T -> Latex.text
-  val pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text
+  val pretty_source: Proof.context -> Token.src -> Pretty.T -> Latex.text
   val pretty_items: Proof.context -> Pretty.T list -> Latex.text
-  val pretty_items_source: Proof.context -> {embedded: bool} -> Token.src ->
-    Pretty.T list -> Latex.text
+  val pretty_items_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
   val antiquotation_pretty:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
-  val antiquotation_pretty_embedded:
-    binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_pretty_source:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
-  val antiquotation_pretty_source_embedded:
-    binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_raw:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
-  val antiquotation_raw_embedded:
-    binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
   val antiquotation_verbatim:
     binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
-  val antiquotation_verbatim_embedded:
-    binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
 end;
 
 structure Thy_Output: THY_OUTPUT =
@@ -62,8 +53,8 @@ fun output_comment ctxt (kind, syms) =
       Symbol_Pos.cartouche_content syms
       |> output_symbols
       |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
-  | Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)]
-  | Comment.Marker => [])
+  | Comment.Latex =>
+      [Latex.symbols (Symbol_Pos.cartouche_content syms)])
 and output_comment_document ctxt (comment, syms) =
   (case comment of
     SOME kind => output_comment ctxt (kind, syms)
@@ -140,7 +131,6 @@ fun output_token ctxt tok =
   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)
@@ -162,7 +152,7 @@ fun check_comments ctxt =
       val pos = #1 (Symbol_Pos.range syms);
       val _ =
         comment |> Option.app (fn kind =>
-          Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups kind)));
+          Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind)));
       val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
     in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
 
@@ -172,6 +162,15 @@ end;
 
 (** present theory source **)
 
+(*NB: arranging white space around command spans is a black art*)
+
+val is_white = Token.is_space orf Token.is_informal_comment;
+val is_black = not o is_white;
+
+val is_white_comment = Token.is_informal_comment;
+val is_black_comment = Token.is_formal_comment;
+
+
 (* presentation tokens *)
 
 datatype token =
@@ -184,8 +183,8 @@ datatype token =
 fun basic_token pred (Basic_Token tok) = pred tok
   | basic_token _ _ = false;
 
-val white_token = basic_token Document_Source.is_white;
-val white_comment_token = basic_token Document_Source.is_white_comment;
+val white_token = basic_token is_white;
+val white_comment_token = basic_token is_white_comment;
 val blank_token = basic_token Token.is_blank;
 val newline_token = basic_token Token.is_newline;
 
@@ -204,7 +203,7 @@ fun present_token ctxt tok =
 
 (* command spans *)
 
-type command = string * Position.T;   (*name, position*)
+type command = string * Position.T * string list;   (*name, position, tags*)
 type source = (token * (string * int)) list;        (*token, markup flag, meta-comment depth*)
 
 datatype span = Span of command * (source * source * source * source) * bool;
@@ -228,8 +227,8 @@ fun make_span cmd src =
 
 local
 
-fun err_bad_nesting here =
-  error ("Bad nesting of commands in presentation" ^ here);
+fun err_bad_nesting pos =
+  error ("Bad nesting of commands in presentation" ^ pos);
 
 fun edge which f (x: string option, y) =
   if x = y then I
@@ -240,23 +239,6 @@ val end_tag = edge #1 Latex.end_tag;
 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' tagging_stack =
-  let
-    val ctxt' = Toplevel.presentation_context state';
-    val nesting = Toplevel.level state' - Toplevel.level state;
-
-    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) taggings of
-          tg :: tgs => (tg, tgs)
-        | [] => err_bad_nesting (Position.here cmd_pos));
-  in (tag', tagging_stack') end;
-
 fun read_tag s =
   (case space_explode "%" s of
     ["", b] => (SOME b, NONE)
@@ -272,44 +254,61 @@ fun make_command_tag options keywords =
     val document_tags_default = map_filter #1 document_tags;
     val document_tags_command = map_filter #2 document_tags;
   in
-    fn cmd_name => fn state => fn state' => fn active_tag =>
+    fn {cmd_name, cmd_tags, tag, active_tag} => fn state => fn state' =>
       let
+        val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
+
         val keyword_tags =
           if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"]
           else Keyword.command_tags keywords cmd_name;
         val command_tags =
           the_list (AList.lookup (op =) document_tags_command cmd_name) @
           keyword_tags @ document_tags_default;
+
         val active_tag' =
-          (case command_tags of
-            default_tag :: _ => SOME default_tag
-          | [] =>
-              if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
-              then active_tag
-              else NONE);
-      in active_tag' end
+          if is_some tag' then tag'
+          else
+            (case command_tags of
+              default_tag :: _ => SOME default_tag
+            | [] =>
+                if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
+                then active_tag
+                else NONE);
+      in {tag' = tag', active_tag' = active_tag'} end
   end;
 
-fun present_span command_tag span state state'
-    (tagging_stack, active_tag, newline, latex, present_cont) =
+fun present_span thy command_tag span state state'
+    (tag_stack, active_tag, newline, latex, present_cont) =
   let
-    val ctxt' = Toplevel.presentation_context state';
+    val ctxt' =
+      Toplevel.presentation_context state'
+        handle Toplevel.UNDEF => Proof_Context.get_global thy Context.PureN;
     val present = fold (fn (tok, (flag, 0)) =>
         fold cons (present_token ctxt' tok)
         #> cons (Latex.string flag)
       | _ => I);
 
-    val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
+    val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
 
-    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 (tag, tags) = tag_stack;
+    val {tag', active_tag'} =
+      command_tag {cmd_name = cmd_name, cmd_tags = cmd_tags, tag = tag, active_tag = active_tag}
+        state state';
     val edge = (active_tag, active_tag');
 
+    val nesting = Toplevel.level state' - Toplevel.level state;
+
     val newline' =
       if is_none active_tag' then span_newline else newline;
 
+    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)
+      else
+        (case drop (~ nesting - 1) tags of
+          tg :: tgs => (tg, tgs)
+        | [] => err_bad_nesting (Position.here cmd_pos));
+
     val latex' =
       latex
       |> end_tag edge
@@ -321,7 +320,7 @@ fun present_span command_tag span state state'
     val present_cont' =
       if newline then (present (#3 srcs), present (#4 srcs))
       else (I, present (#3 srcs) #> present (#4 srcs));
-  in (tagging_stack', active_tag', newline', latex', present_cont') end;
+  in (tag_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"
@@ -341,6 +340,14 @@ local
 val markup_true = "\\isamarkuptrue%\n";
 val markup_false = "\\isamarkupfalse%\n";
 
+val space_proper =
+  Scan.one Token.is_blank -- Scan.many is_white_comment -- Scan.one is_black;
+
+val is_improper = not o (is_black orf Token.is_begin_ignore orf Token.is_end_ignore);
+val improper = Scan.many is_improper;
+val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
+val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
+
 val opt_newline = Scan.option (Scan.one Token.is_newline);
 
 val ignore =
@@ -350,10 +357,11 @@ val ignore =
     (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
     >> pair (d - 1));
 
+val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
+
 val locale =
-  Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |--
-    Parse.!!!
-      (Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")")));
+  Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
+    Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
 
 in
 
@@ -370,26 +378,25 @@ fun present_thy options thy (segments: segment list) =
       >> (fn d => (NONE, (Ignore_Token, ("", d))));
 
     fun markup pred mk flag = Scan.peek (fn d =>
-      Document_Source.improper |--
+      improper |--
         Parse.position (Scan.one (fn tok =>
           Token.is_command tok andalso pred keywords (Token.content_of tok))) --
-      (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));
+      Scan.repeat tag --
+      Parse.!!!! ((improper -- locale -- improper) |-- Parse.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));
 
     val command = Scan.peek (fn d =>
-      Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
-      Scan.one Token.is_command --| Document_Source.annotation
-      >> (fn (cmd_mod, cmd) =>
+      Scan.optional (Scan.one Token.is_command_modifier ::: improper) [] --
+      Scan.one Token.is_command -- Scan.repeat tag
+      >> (fn ((cmd_mod, cmd), tags) =>
         map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
-          [(SOME (Token.content_of cmd, Token.pos_of cmd),
+          [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
             (Basic_Token cmd, (markup_false, d)))]));
 
     val cmt = Scan.peek (fn d =>
-      Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
+      Scan.one is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
 
     val other = Scan.peek (fn d =>
        Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
@@ -444,14 +451,14 @@ fun present_thy options thy (segments: segment list) =
     val command_tag = make_command_tag options keywords;
 
     fun present_command tr span st st' =
-      Toplevel.setmp_thread_position tr (present_span command_tag span st st');
+      Toplevel.setmp_thread_position tr (present_span thy command_tag span st st');
 
     fun present _ [] = I
       | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
   in
     if length command_results = length spans then
-      (([], []), NONE, true, [], (I, I))
-      |> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
+      ((NONE, []), NONE, true, [], (I, I))
+      |> present Toplevel.toplevel (spans ~~ command_results)
       |> present_trailer
       |> rev
     else error "Messed-up outer syntax for presentation"
@@ -494,19 +501,9 @@ fun verbatim ctxt =
   then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
   else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
 
-fun token_source ctxt {embedded} tok =
-  if Token.is_kind Token.Cartouche tok andalso embedded andalso
-    not (Config.get ctxt Document_Antiquotation.thy_output_source_cartouche)
-  then Token.content_of tok
-  else Token.unparse tok;
-
-fun is_source ctxt =
-  Config.get ctxt Document_Antiquotation.thy_output_source orelse
-  Config.get ctxt Document_Antiquotation.thy_output_source_cartouche;
-
-fun source ctxt embedded =
+fun source ctxt =
   Token.args_of_src
-  #> map (token_source ctxt embedded #> Document_Antiquotation.prepare_lines ctxt)
+  #> map (Token.unparse #> Document_Antiquotation.prepare_lines ctxt)
   #> space_implode " "
   #> output_source ctxt
   #> isabelle ctxt;
@@ -514,53 +511,33 @@ fun source ctxt embedded =
 fun pretty ctxt =
   Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt;
 
-fun pretty_source ctxt embedded src prt =
-  if is_source ctxt then source ctxt embedded src else pretty ctxt prt;
+fun pretty_source ctxt src prt =
+  if Config.get ctxt Document_Antiquotation.thy_output_source
+  then source ctxt src else pretty ctxt prt;
 
 fun pretty_items ctxt =
   map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt;
 
-fun pretty_items_source ctxt embedded src prts =
-  if is_source ctxt then source ctxt embedded src else pretty_items ctxt prts;
+fun pretty_items_source ctxt src prts =
+  if Config.get ctxt Document_Antiquotation.thy_output_source
+  then source ctxt src else pretty_items ctxt prts;
 
 
 (* antiquotation variants *)
 
-local
+fun antiquotation_pretty name scan f =
+  Document_Antiquotation.setup name scan
+    (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
 
-fun gen_setup name embedded =
-  if embedded
-  then Document_Antiquotation.setup_embedded name
-  else Document_Antiquotation.setup name;
+fun antiquotation_pretty_source name scan f =
+  Document_Antiquotation.setup name scan
+    (fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x));
 
-fun gen_antiquotation_pretty name embedded scan f =
-  gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
+fun antiquotation_raw name scan f =
+  Document_Antiquotation.setup name scan
+    (fn {context = ctxt, argument = x, ...} => f ctxt x);
 
-fun gen_antiquotation_pretty_source name embedded scan f =
-  gen_setup name embedded scan
-    (fn {context = ctxt, source = src, argument = x} =>
-      pretty_source ctxt {embedded = embedded} src (f ctxt x));
-
-fun gen_antiquotation_raw name embedded scan f =
-  gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);
-
-fun gen_antiquotation_verbatim name embedded scan f =
-  gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt);
-
-in
-
-fun antiquotation_pretty name = gen_antiquotation_pretty name false;
-fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true;
-
-fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false;
-fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true;
-
-fun antiquotation_raw name = gen_antiquotation_raw name false;
-fun antiquotation_raw_embedded name = gen_antiquotation_raw name true;
-
-fun antiquotation_verbatim name = gen_antiquotation_verbatim name false;
-fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true;
-
-end;
+fun antiquotation_verbatim name scan f =
+  antiquotation_raw name scan (fn ctxt => verbatim ctxt o f ctxt);
 
 end;