Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF

examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy

@@ -505,9 +505,6 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-
                       caption2="''Exploring an attribute (hyperlinked to the class).''",
                       relative_width2="47",
                       src2="''figures/Dogfood-V-attribute''"]\<open>Navigation via generated hyperlinks.\<close>
-(* TODO: Update the images in fig:Dogfood-IV-jumpInDocCLass side_by_side_figure
-   to align them. This has to wait that the exploration of an attribute is again possible.
-   See: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/issues/10 *)
 
 text\<open> 
   From these class definitions, \<^isadof> also automatically generated editing 

examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy

@@ -331,7 +331,7 @@ is currently only available in the SML API's of the kernel.
   symbolic evaluation using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
   evaluation\<close> and \<^emph>\<open>code\<close> for code generation in SML.
 \<^item> \<open>upd_meta_args\<close> :
-   \<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
+   \<^rail>\<open> (obj_id ('::' class_id) ((',' attribute (':=' | '+=') HOL_term) * ))\<close>
 \<^item> \<open>annotated_text_element\<close> :
 \<^rail>\<open> 
     (  @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
@@ -1009,9 +1009,6 @@ text\<open>
   these types. They are just types declared in HOL, 
   which are ``inhabited'' by special constant symbols carrying strings, for
   example of the format \<^boxed_theory_text>\<open>@{thm <string>}\<close>.
-  % TODO:
-  % Update meta-types implementation explanation to the new implementation
-  % in repository commit 08c101c5440eee2a087068581952026e88c39f6a
   When HOL
   expressions were used to denote values of \<^boxed_theory_text>\<open>doc_class\<close>
   instance attributes, this requires additional checks after

src/DOF/Isa_DOF.thy

@@ -1244,13 +1244,34 @@ fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init
 
 fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long
                      (S:(string * Position.T * string * term)list) term = 
-    let val cid_ty = cid_2_cidType cid_long thy 
+    let val cid_ty = cid_2_cidType cid_long thy
         val generalize_term =  Term.map_types (generalize_typ 0)
         fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t  
         fun instantiate_term S t =
           Term_Subst.map_types_same (Term_Subst.instantiateT (TVars.make S)) (t)
         fun read_assn (lhs, pos:Position.T, opr, rhs) term =
-            let val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy
+            let 
+                fun get_class_name parent_cid attribute_name pos =
+                  let
+                    val {attribute_decl, inherits_from, ...} =
+                                                   the (DOF_core.get_doc_class_global parent_cid thy)
+                  in
+                    if exists (fn (binding, _, _) => Binding.name_of binding = attribute_name)
+                              attribute_decl
+                    then parent_cid
+                    else
+                      case inherits_from of
+                          NONE =>
+                                ISA_core.err ("Attribute not defined for class: " ^ cid_long) pos
+                        | SOME (_, parent_name) =>
+                                              get_class_name parent_name attribute_name pos
+                  end
+                val attr_defined_cid = get_class_name cid_long lhs pos
+                val {id, name, ...} = the (DOF_core.get_doc_class_global attr_defined_cid thy)
+                val markup = docclass_markup false cid_long id (Binding.pos_of name);
+                val ctxt = Context.Theory thy
+                val _    = Context_Position.report_generic ctxt pos markup;
+                val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy
                 val (ln,lnt,lnu,lnut) = case info_opt of 
                                            NONE => error ("unknown attribute >" 
                                                           ^((Long_Name.base_name lhs))
@@ -1353,14 +1374,11 @@ fun check_invariants thy oid =
   let
     val value = the (DOF_core.get_value_global oid thy)
     val cid = #cid (the (DOF_core.get_object_global oid thy))
-    (*val _ = writeln ("cid: " ^ @{make_string} (Long_Name.base_name cid))*)
     fun get_all_invariants cid thy =
-      let val invs = #invs (the (DOF_core.get_doc_class_global cid thy))
-      in case DOF_core.get_doc_class_global cid thy of
-             NONE => error("undefined class id for invariants: " ^ cid)
-           | SOME ({inherits_from=NONE, ...}) => invs
-           | SOME ({inherits_from=SOME(_,father), ...}) => (invs) @ (get_all_invariants father thy)
-      end
+       case DOF_core.get_doc_class_global cid thy of
+          NONE => error("undefined class id for invariants: " ^ cid)
+        | SOME ({inherits_from=NONE, invs, ...}) => invs
+        | SOME ({inherits_from=SOME(_,father), invs, ...}) => (invs) @ (get_all_invariants father thy)
     val invariants = get_all_invariants cid thy
     val inv_and_apply_list = 
       let fun mk_inv_and_apply inv value thy =
@@ -2008,7 +2026,7 @@ fun print_doc_items b ctxt =
                   writeln ("    type:            "^cid);
                   case vcid of NONE => () | SOME (s) => 
                   writeln ("    virtual type:    "^ s);
-                  writeln ("    origine:         "^thy_name);
+                  writeln ("    origin:          "^thy_name);
                   writeln ("    inline:          "^dfg inline);
                   writeln ("    input_term:      "
                            ^ (Syntax.string_of_term

src/ontologies/scholarly_paper/scholarly_paper.thy

@@ -305,7 +305,7 @@ val _ =
     {markdown = true, body = true}
     (fn meta_args => fn thy =>
       let
-        val ddc = Config.get_global thy Definition_default_class
+        val ddc = Config.get_global thy Lemma_default_class
         val use_Lemma_default = SOME(((ddc = "") ? (K "math_content")) ddc)
       in
         Onto_Macros.enriched_formal_statement_command
@@ -317,7 +317,7 @@ val _ =
     {markdown = true, body = true}
     (fn meta_args => fn thy =>
       let
-        val ddc = Config.get_global thy Definition_default_class
+        val ddc = Config.get_global thy Theorem_default_class
         val use_Theorem_default = SOME(((ddc = "") ? (K "math_content")) ddc)
       in
         Onto_Macros.enriched_formal_statement_command