refinements of the technical class; added the document antiquotation doc_class; some experiments in SI.

src/DOF/Isa_COL.thy

@@ -104,7 +104,7 @@ doc_class concept =
     properties :: "thm list" <= "[]"
 
 section\<open>Tests\<close>
-
+   
 ML\<open>@{term "side_by_side_figure"};
 @{typ "doc_class rexp"}; 
 DOF_core.SPY;

src/DOF/Isa_DOF.thy

@@ -1675,8 +1675,11 @@ fun compute_trace_ML ctxt oid pos pos' =
     in  map conv (HOLogic.dest_list term) end
 
 val parse_oid = Scan.lift(Parse.position Args.name) 
+val parse_cid = Scan.lift(Parse.position Args.name) 
 val parse_oid' = Term_Style.parse -- parse_oid
-val parse_attribute_access = (parse_oid 
+val parse_cid' = Term_Style.parse -- parse_cid
+
+val parse_attribute_access = (parse_oid
                               --| (Scan.lift @{keyword "::"}) 
                               -- Scan.lift (Parse.position Args.name))
                               : ((string *Position.T) * (string * Position.T)) context_parser 
@@ -1693,6 +1696,10 @@ fun trace_attr_2_ML ctxt (oid:string,pos) =
         val toML = (ML_Syntax.atomic o (ML_Syntax.print_list print_string_pair))
     in  toML (compute_trace_ML ctxt oid @{here} pos) end
 
+fun compute_cid_repr ctxt cid pos = 
+      if DOF_core.is_defined_cid_local  cid ctxt then Const(cid,dummyT)
+      else ISA_core.err "Undefined Class Id" pos
+
 local
 
 fun pretty_attr_access_style ctxt (style, ((oid,pos),(attr,pos'))) = 
@@ -1701,13 +1708,17 @@ fun pretty_attr_access_style ctxt (style, ((oid,pos),(attr,pos'))) =
 fun pretty_trace_style ctxt (style, (oid,pos)) = 
           Thy_Output.pretty_term ctxt (style (compute_attr_access  (Context.Proof ctxt) 
                                                                    "trace" oid pos pos));
-in  
+fun pretty_cid_style ctxt (style, (cid,pos)) = 
+          Thy_Output.pretty_term ctxt (style (compute_cid_repr ctxt cid pos));
+
+in
 val _ = Theory.setup 
            (ML_Antiquotation.inline  \<^binding>\<open>docitem_attribute\<close> 
                (fn (ctxt,toks) => (parse_attribute_access >>  attr_2_ML ctxt) (ctxt, toks))  #>
             ML_Antiquotation.inline  \<^binding>\<open>trace_attribute\<close>  
                (fn (ctxt,toks) => (parse_oid >> trace_attr_2_ML ctxt) (ctxt, toks)) #>
             basic_entity  \<^binding>\<open>trace_attribute\<close>  parse_oid'  pretty_trace_style #>
+            basic_entity  \<^binding>\<open>doc_class\<close>  parse_cid'  pretty_cid_style #>
             basic_entity  \<^binding>\<open>docitem_attribute\<close>  parse_attribute_access' pretty_attr_access_style
            )
 end

src/SI/Units.thy

@@ -118,17 +118,19 @@ proof
 qed
 
 
-
-instance SI_domain_ext :: (field) field
+(*
+instance SI_domain_ext :: ("{field,inverse}") field
 proof
-  fix a b :: "'a SI_domain_ext"
+  fix a b :: "'a::field SI_domain_ext"
   show "inverse a \<cdot> a  = 1"
+    unfolding inverse_SI_domain_ext_def times_SI_domain_ext_def one_SI_domain_ext_def
+    apply auto
     sledgehammer
     by (simp add: inverse_SI_domain_ext_def times_SI_domain_ext_def one_SI_domain_ext_def)
   show "a \<cdot> inverse b = a div b"
     by (simp add: divide_SI_domain_ext_def)
 qed
-
+*)
 
 
 
@@ -800,7 +802,7 @@ lemma "watt *\<^sub>U hour \<approx>\<^sub>U 3600 *\<^sub>U joule"
   thm Units.Unit.toUnit_inverse
 
 
-lemma "watt *\<^sub>U hour \<approx>\<^sub>U 3.6 *\<^sub>U kilo *\<^sub>U joule"
+lemma "watt *\<^sub>U hour = 3.6 *\<^sub>U kilo *\<^sub>U joule"
   oops
 
 end

src/ontologies/scholarly_paper/scholarly_paper.thy

@@ -54,15 +54,52 @@ doc_class introduction = text_section +
    comment :: string
    claims  :: "thm list"
 
+text\<open>Technical text-elements posses a status: they can be either an \<^emph>\<open>informal explanation\<close> /
+description or a kind of introductory text to definition etc. or a \<^emph>\<open>formal statement\<close> similar
+to :
+
+\<^bold>\<open>Definition\<close> 3.1: Security. 
+As Security of the system we define etc...
+
+A formal statement can, but must not have a reference to true formal Isabelle/Isar definition. 
+\<close>
+datatype status = formal | description
+
 doc_class technical = text_section +
    definition_list :: "string list" <=  "[]"
+   status :: status <= "description"
    formal_results  :: "thm list"
    
 text\<open>A very rough formatting style could be modeled as follows:\<close>   
 
-   
-doc_class example    = text_section +
-   comment :: "string"
+
+doc_class "experiment"  = technical +
+   tag :: "string" <=  "''''"
+
+doc_class example       = technical +
+   tag :: "string" <=  "''''"
+
+doc_class "definition"  = technical +
+   tag :: "string" <=  "''''"
+
+doc_class "theorem"     = technical +
+   tag :: "string" <=  "''''"
+
+doc_class "code"     = technical +
+   checked :: bool <=  "False"
+   tag :: "string" <=  "''''"
+
+text\<open>The @{doc_class "code"} is a general stub for free-form and type-checked code-fragments
+such as:
+\<^enum> SML code
+\<^enum> bash code
+\<^enum> isar code (although this might be an unwanted concurrence to the Isabelle standard cartouche)
+\<^enum> C code.
+
+it is intended that later refinements of this "stub" as done in \<^verbatim>\<open>Isabelle_C\<close> which come with their
+own content checking and, of course, presentation styles. 
+\<close>
+
 
 doc_class "conclusion" = text_section +
    main_author :: "author option"  <=  None
@@ -198,5 +235,6 @@ fun check_group a = map (check_group_elem (check_level_hd (hd a))) (tl a) ;
 *)
 \<close>
 
+
 end