Trace-Calculation refined. One gets the additional information WHICH oid of which class

is added to the trace.

Isa_DOF.thy

@@ -863,7 +863,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy =
           fun markup2string x = XML.content_of (YXML.parse_body x)
           fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn, 
                                                      Syntax.read_term_global thy rhs)
-          val trace_attr = [((("trace", @{here}), "+="), "["^cid_long^"]")]
+          val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")]
           val assns' = map conv_attrs trace_attr
           fun cid_of oid = #cid(the(DOF_core.get_object_global oid thy))
           fun def_trans oid = #1 o (calc_update_term thy (cid_of oid) assns')
@@ -936,7 +936,8 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta
 
 
 fun open_monitor_command  ((((oid,pos),cid_pos), doc_attrs) : meta_args_t) =
-    let fun o_m_c oid pos cid_pos doc_attrs thy = create_and_check_docitem true oid pos cid_pos doc_attrs thy
+    let fun o_m_c oid pos cid_pos doc_attrs thy = create_and_check_docitem true oid pos 
+                                                                           cid_pos doc_attrs thy
         val add_consts = fold_aterms (fn Const(c as (_,@{typ "doc_class rexp"})) => insert (op =) c 
                                         | _ => I);
         fun compute_enabled_set cid thy = 
@@ -1297,7 +1298,7 @@ fun read_fields raw_fields ctxt =
 
 
 val tag_attr = (Binding.make("tag_attribute",@{here}), @{typ "int"},Mixfix.NoSyn)
-val trace_attr = ((Binding.make("trace",@{here}), "doc_class rexp list",Mixfix.NoSyn),
+val trace_attr = ((Binding.make("trace",@{here}), "(doc_class rexp \<times> string) list",Mixfix.NoSyn),
                   SOME "[]"): ((binding * string * mixfix) * string option)
 
 fun check_regexps term = 
@@ -1390,7 +1391,7 @@ doc_class side_by_side_figure = figure +
    caption2         :: "string"
 
 doc_class figure_group = 
-   trace            :: "doc_class rexp list" <= "[]"
+ (*  trace            :: "doc_class rexp list" <= "[]" *)
    anchor           :: "string"
    caption          :: "string"
    where "\<lbrace>figure\<rbrace>\<^sup>+"
@@ -1418,7 +1419,7 @@ writeln (DOF_core.toStringDocItemRef "scholarly_paper.introduction" "XX" []);
 *)
 
 ML\<open> fold_aterms  Term.add_free_names;
-fold_aterms  Term.add_var_names;
+    fold_aterms  Term.add_var_names;
 \<close>
 
 

examples/conceptual/Attributes.thy

@@ -23,6 +23,9 @@ text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\<open> sdfsdfs sdfsdf
 
 typ "C"
 typ "D"
+
+term "C"
+
 ML\<open>val Type("Conceptual.B.B_ext",[Type("Conceptual.C.C_ext",t)]) = @{typ "C"};
    val @{typ "D"} = ODL_Command_Parser.cid_2_cidType "Conceptual.D" @{theory};
    val @{typ "E"}= ODL_Command_Parser.cid_2_cidType "Conceptual.E" @{theory};
@@ -114,7 +117,13 @@ figure*[fig_B::figure,
 close_monitor*[figs1]  
 
 text\<open>Resulting trace in figs1: \<close>
-ML\<open> map (fn Const(s,_) => s) (HOLogic.dest_list @{docitem_attr trace::figs1}) \<close>
+ML\<open> fun conv_doc_class_string_pair (Const(@{const_name "Pair"},_) 
+                                    $ Const(s,_) 
+                                    $ S) = (s, HOLogic.dest_string S);
+
+map  conv_doc_class_string_pair (HOLogic.dest_list @{docitem_attr trace::figs1}) \<close>
+
+
 
 print_doc_items
 print_doc_classes 

examples/scholarly/IsaDofApplications.thy

@@ -737,8 +737,13 @@ and therefore granted with public funds within the scope of the Program ``Invest
 (*<*) 
 close_monitor*[this]
 
-text\<open>Resulting trace in figs1: \<close>
-ML\<open> map (fn Const(s,_) => s) (HOLogic.dest_list @{docitem_attr trace::this}) \<close>
+text\<open>Resulting trace in this: \<close>
+ML\<open> 
+fun conv_doc_class_string_pair (Const(@{const_name "Pair"},_) 
+                                    $ Const(s,_) 
+                                    $ S) = (s, HOLogic.dest_string S);
+
+map conv_doc_class_string_pair (HOLogic.dest_list @{docitem_attr trace::this}) \<close>
 
 end
 (*>*) 

ontologies/scholarly_paper.thy

@@ -48,43 +48,43 @@ doc_class related_work = "conclusion" +
 doc_class bibliography =
    style :: "string option"  <=  "Some ''LNCS''"
 
-text{* Besides subtyping, there is another relation between
-       doc_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
-       which is expressed by occurrence in the where clause.
-       While sub-classing refers to data-inheritance of attributes,
-       a monitor captures structural constraints -- the order --
-       in which instances of monitored classes may occur.
+text\<open> Besides subtyping, there is another relation between
+doc_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
+which is expressed by occurrence in the where clause.
+While sub-classing refers to data-inheritance of attributes,
+a monitor captures structural constraints -- the order --
+in which instances of monitored classes may occur.
 
-       The control of monitors is done by the commands:
-       \<^item> monitor <doc-class>
-       \<^item> close_monitor <doc-class>
- 
-       where the automaton of the monitor class is expected
-       to be in a final state.
+The control of monitors is done by the commands:
+\<^item> \<^verbatim>\<open> monitor <oid::class_type, <attributes-defs> > \<close>
+\<^item> \<^verbatim>\<open> close_monitor <oid[::class_type],<attributes-updates>> \<close>
 
-       Monitors can be nested.
- 
-       Classes neither directly or via inheritance indirectly
-       mentioned in the monitor are \<^emph>\<open>independent\<close> from
-       a monitor and may occur freely. 
-*}
+where the automaton of the monitor class is expected
+to be in a final state.
+
+Monitors can be nested.
+
+Classes neither directly or  indirectly (via inheritance)
+mentioned in the monitor clause are \<^emph>\<open>independent\<close> from
+the monitor and may occur freely, \ie{} in arbitrary order.n \<close>
 
 
--- \<open>underlying idea: capture the essence of a monitor class as trace.
-    trace would be \<^emph>\<open>`predefined id`\<close> like \<^verbatim>\<open>main\<close> in C. \<close>
-text{* @{cite bla} *}
+text \<open>underlying idea: a monitor class automatically receives a  
+    \<^verbatim>\<open>trace\<close> attribute in which a list of observed class-ids is maintained.
+    The \<^verbatim>\<open>trace\<close> is a \<^emph>\<open>`predefined id`\<close> like \<^verbatim>\<open>main\<close> in C. It can be accessed
+    like any other attribute of a class instance, \ie{} a document item.\<close>
 
 doc_class article = 
    style_id :: string                <= "''LNCS''"
    version  :: "(int \<times> int \<times> int)"  <= "(0,0,0)"
    where "(title       ~~ 
            \<lbrakk>subtitle\<rbrakk>   ~~
-           \<lbrace>author\<rbrace>\<^sup>+    ~~ 
+           \<lbrace>author\<rbrace>\<^sup>+   ~~ 
            abstract     ~~
            introduction ~~ 
            \<lbrace>technical || example\<rbrace>\<^sup>+ ~~ 
            conclusion   ~~  
-           \<lbrakk>bibliography\<rbrakk>)"
+           bibliography)"
 
 gen_sty_template