diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index d30cd8e..dd184e5 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -56,7 +56,7 @@ fun docref_markup_gen refN def name id pos =
   if id = 0 then Markup.empty
   else
     Markup.properties (Position.entity_properties_of def id pos)
-      (Markup.entity refN name);   (* or better store the thy-name as property ? ? ? *)
+                      (Markup.entity refN name);   (* or better store the thy-name as property ? ? ? *)
 
 val docref_markup = docref_markup_gen docrefN
 
@@ -746,12 +746,91 @@ consts ISA_thy          :: "string \<Rightarrow> thy"               ("@{thy _}")
 consts ISA_docitem      :: "string \<Rightarrow> 'a"                ("@{docitem _}")
 consts ISA_docitem_attr :: "string \<Rightarrow> string \<Rightarrow> 'a"      ("@{docitemattr (_) :: (_)}")
 
+\<comment> \<open>Dynamic setup of inner syntax cartouche\<close>
+
+ML \<open>
+(*  Author:     Frédéric Tuong, Université Paris-Saclay *)
+(*  Title:      HOL/ex/Cartouche_Examples.thy
+    Author:     Makarius
+*)
+  local
+    fun mk_char f_char (s, _) accu =
+        fold
+          (fn c => fn (accu, l) =>
+            (f_char c accu,
+               Syntax.const @{const_syntax Cons}
+             $ (Syntax.const @{const_syntax Char} $ HOLogic.mk_numeral c)
+             $ l))
+          (rev (map Char.ord (String.explode s)))
+          accu;
+
+    fun mk_string _ accu [] = (accu, Const (@{const_syntax Nil}, @{typ "char list"}))
+      | mk_string f_char accu (s :: ss) = mk_char f_char s (mk_string f_char accu ss);
+
+  in
+    fun string_tr f f_char accu content args =
+      let fun err () = raise TERM ("string_tr", args) in
+        (case args of
+          [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
+            (case Term_Position.decode_position p of
+              SOME (pos, _) => c $ f (mk_string f_char accu (content (s, pos))) $ p
+            | NONE => err ())
+        | _ => err ())
+      end;
+  end;
+\<close>
+
+syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> _"  ("_")
+
+ML\<open>
+val cartouche_grammar =
+  [ ("char list", snd)
+  , ("String.literal", (fn (_, x) => Syntax.const @{const_syntax STR} $ x))]
+\<close>
+
+ML\<open>
+fun parse_translation_cartouche binding l f_char accu =
+  let val cartouche_type = Attrib.setup_config_string binding (K (fst (hd l)))
+      (* if there is no type specified, by default we set the first element
+         to be the default type of cartouches *) in
+  fn ctxt =>
+    string_tr
+      let val cart_type = Config.get ctxt cartouche_type in
+      case (List.find (fn (s, _) => s = cart_type)
+                          l) of
+        NONE => error ("Unregistered return type for the cartouche: \"" ^ cart_type ^ "\"")
+      | SOME (_, f) => f
+      end
+      f_char
+      accu
+      (Symbol_Pos.cartouche_content o Symbol_Pos.explode)
+  end
+\<close>
+
+parse_translation \<open>
+  [( @{syntax_const "_cartouche_string"}
+   , parse_translation_cartouche @{binding cartouche_type} cartouche_grammar (K I) ())]
+\<close>
+
+
 (* tests *)  
 term "@{typ  ''int => int''}"  
 term "@{term ''Bound 0''}"  
 term "@{thm  ''refl''}"  
 term "@{docitem  ''<doc_ref>''}"
 ML\<open>   @{term "@{docitem  ''<doc_ref>''}"}\<close>
+(**)
+term "@{typ  \<open>int => int\<close>}"  
+term "@{term \<open>Bound 0\<close>}"  
+term "@{thm  \<open>refl\<close>}"  
+term "@{docitem  \<open><doc_ref>\<close>}"
+ML\<open>   @{term "@{docitem  \<open><doc_ref>\<close>}"}\<close>
+(**)
+declare [[cartouche_type = "String.literal"]]
+term "\<open>Université\<close> :: String.literal"
+declare [[cartouche_type = "char list"]]
+term "\<open>Université\<close> :: char list"
+(**)
 
 
 subsection\<open> Semantics \<close>
@@ -1446,7 +1525,7 @@ val docitem_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc
                                                  else {unchecked = true,  define= false})) 
                                    {unchecked = false, define= false} (* default *);
 
-val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.cartouche_input))
+val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input))
 
 fun docitem_antiquotation_generic cid_decl 
              {context = ctxt, source = src:Token.src, state}  
diff --git a/examples/conceptual/Concept_Example.thy b/examples/conceptual/Concept_Example.thy
index 8085c0c..935f1cb 100644
--- a/examples/conceptual/Concept_Example.thy
+++ b/examples/conceptual/Concept_Example.thy
@@ -14,7 +14,7 @@ section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
 text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ...  \<close>
 
 text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, 
-                         ... @{docitem \<open>c1\<close>} @{thm "refl"}\<close>
+                         ... @{docitem c1} @{thm "refl"}\<close>
 
 
 update_instance*[d::D, a1 := X2]
@@ -35,12 +35,13 @@ text\<open> ..., mauris amet, id elit aliquam aptent id,  ... @{docitem \<open>a
 text\<open>Here we add and maintain a link that is actually modeled as m-to-n relation ...\<close>
 update_instance*[f::F,b:="{(@{docitem  ''a''}::A,@{docitem  ''c1''}::C), 
                            (@{docitem  ''a''},   @{docitem  ''c2''})}"] 
-  
+
 close_monitor*[struct]
 
 text\<open>And the trace of the monitor is:\<close>
 ML\<open>@{trace_attribute struct}\<close>
 
+
 print_doc_classes
 print_doc_items
 
diff --git a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy
index 4b4fa43..e6b3074 100644
--- a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy
+++ b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy
@@ -9,7 +9,7 @@ open_monitor*[this::report]
 
 title*[tit::title]\<open>An Account with my Personal, Ecclectic Comments on the Isabelle Architecture\<close> 
 subtitle*[stit::subtitle]\<open>Version : Isabelle 2017\<close>
-text*[bu::author,
+text*[bu::author,     
       email       = "''wolff@lri.fr''",
       affiliation = "''Universit\\'e Paris-Saclay, Paris, France''"]\<open>Burkhart Wolff\<close>
     
@@ -845,6 +845,8 @@ end;
 *)
 \<close>
 
+
+
   
 ML\<open> Thy_Output.document_command {markdown = true} \<close>  
 (* Structures related to LaTeX Generation *)
@@ -1158,15 +1160,68 @@ ML\<open> fun dark_matter x = XML.content_of (YXML.parse_body x)\<close>
 
 (* MORE TO COME *)
 
+section\<open>Positions\<close>
+text\<open>A basic data-structure relevant for PIDE are \<^emph>\<open>positions\<close>; beyond the usual line- and column
+information they can represent ranges, list of ranges, and the name of the atomic sub-document
+in which they are contained. In the command:\<close>
+ML\<open>
+val pos = @{here};
+val markup = Position.here pos;
+writeln ("And a link to the declaration of 'here' is "^markup)
+\<close> 
+(* \<^here>  *)
+text\<open> ... uses the antiquotation @{ML "@{here}"} to infer from the system lexer the actual position
+of itself in the global document, converts it to markup (a string-representation of it) and sends
+it via the usual @{ML "writeln"} to the interface. \<close>
+
+figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"]
+\<open>Output with hyperlinked position.\<close>
+
+text\<open>@{docitem \<open>hyplinkout\<close>} shows the produced output where the little house-like symbol in the 
+display is hyperlinked to the position of @{ML "@{here}"} in the ML sample above.\<close>
+
+section\<open>Markup and Low-level Markup Reporting\<close>
+text\<open>The structures @{ML_structure Markup} and @{ML_structure Properties} represent the basic 
+annotation data which is part of the protocol sent from Isabelle to the frontend.
+They are qualified as "quasi-abstract", which means they are intended to be an abstraction of 
+the serialized, textual presentation of the protocol. Markups are structurally a pair of a key
+and properties; @{ML_structure Markup} provides a number of of such \<^emph>\<open>key\<close>s for annotation classes
+such as "constant", "fixed", "cartouche", some of them quite obscure. Here is a code sample
+from \<^theory_text>\<open>Isabelle_DOF\<close>. A markup must be tagged with an id; this is done by the @{ML serial}-function
+discussed earlier.\<close>
+ML\<open> 
+local 
+  
+val docclassN = "doc_class";    
+
+(* derived from: theory_markup; def for "defining occurrence" (true) in contrast to
+   "referring occurence" (false). *) 
+fun docclass_markup def name id pos =
+  if id = 0 then Markup.empty
+  else           Markup.properties (Position.entity_properties_of def id pos)
+                                   (Markup.entity docclassN name);   
+
+in
+
+fun report_defining_occurrence pos cid =
+           let val id = serial ()
+               val markup_of_cid = docclass_markup true cid id pos
+           in  Position.report pos markup_of_cid end;
+
+end
+\<close>
+
+text\<open>The @\<open>ML report_defining_occurrence\<close>-function above takes a position and a "cid" parsed
+in the Front-End, converts this into markup together with a unique number identifying this
+markup, and sends this as a report to the Front-End. \<close>
 
-section\<open>Low-level Markup Reporting\<close>
 
 section\<open>Environment Structured Reporting\<close>
 
 text\<open> @{ML_type "'a Name_Space.table"} \<close>
 
 section\<open> Parsing issues \<close>  
-  
+
 text\<open> Parsing combinators represent the ground building blocks of both generic input engines
 as well as the specific Isar framework. They are implemented in the  structure \verb+Token+ 
 providing core type \verb+Token.T+. 
diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT
index bf9d816..2952a4c 100644
--- a/examples/technical_report/TR_my_commented_isabelle/ROOT
+++ b/examples/technical_report/TR_my_commented_isabelle/ROOT
@@ -7,6 +7,7 @@ session "TR_mycommentedisabelle" = "Isabelle_DOF" +
     "preamble.tex"
     "prooftree.sty"
     "build"
+    "figures/markup-demo"
     "figures/text-element.pdf"
     "figures/isabelle-architecture.pdf"
     "figures/pure-inferences-I.pdf"
diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png b/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png
new file mode 100644
index 0000000..661566e
Binary files /dev/null and b/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png differ
diff --git a/ontologies/CENELEC_50128.thy b/ontologies/CENELEC_50128.thy
index b9a6ef4..2d67e64 100644
--- a/ontologies/CENELEC_50128.thy
+++ b/ontologies/CENELEC_50128.thy
@@ -239,7 +239,7 @@ datatype role =  PM  (* Program Manager *)
               |  DES (* Designer *)
               |  IMP (* Implementer *)
               |  ASR (* Assessor *)
-              |  INT  (* Integrator *)
+              |  INT (* Integrator *)
               |  TST (* Tester *)
               |  VER (* Verifier *)
               |  VnV (* Verification and Validation *)
diff --git a/ontologies/small_math.thy b/ontologies/small_math.thy
index 437bc18..fc87679 100644
--- a/ontologies/small_math.thy
+++ b/ontologies/small_math.thy
@@ -99,7 +99,7 @@ text \<open>underlying idea: a monitor class automatically receives a
 
 doc_class article = 
     style_id :: string                <= "''LNCS''"
-    accepts "(title      ~~ \<lbrace>author\<rbrace>\<^sup>+     ~~   abstract      ~~
+    accepts "(title           ~~ \<lbrace>author\<rbrace>\<^sup>+               ~~   abstract      ~~
              \<lbrace>introduction\<rbrace>\<^sup>+  ~~  \<lbrace>technical || example\<rbrace>\<^sup>+ ~~ \<lbrace>conclusion\<rbrace>\<^sup>+)"
 
 
@@ -158,7 +158,6 @@ setup\<open> let val cidS = ["small_math.introduction","small_math.technical", "
 
 
 
-
 gen_sty_template