Something in Isabelle_DOF

Isa_DOF.thy

@@ -1434,7 +1434,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}  

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]
@@ -41,6 +41,7 @@ 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
 

examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy

@@ -846,6 +846,8 @@ end;
 \<close>
 
 
+
+  
 ML\<open> Thy_Output.document_command {markdown = true} \<close>  
 (* Structures related to LaTeX Generation *)
 ML\<open>  Latex.output_ascii;
@@ -1158,8 +1160,61 @@ 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>
 

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"

ontologies/small_math.thy

@@ -158,7 +158,6 @@ setup\<open> let val cidS = ["small_math.introduction","small_math.technical", "
 
 
 
-
 gen_sty_template