1.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml	Fri Jan 06 09:55:35 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml	Fri Jan 06 10:33:16 2023 +0100
     1.3 @@ -22,6 +22,10 @@
     1.4    val Isac: 'a -> theory
     1.5    val parent_of: theory -> theory -> theory
     1.6  
     1.7 +  type metadata
     1.8 +  val the_metadata: theory -> metadata
     1.9 +  val set_metadata: metadata -> theory -> theory
    1.10 +
    1.11  \<^isac_test>\<open>
    1.12    val get_thy: id -> theory            (* restricted to session Isac *)
    1.13  \<close>
    1.14 @@ -70,4 +74,24 @@
    1.15  
    1.16  fun parent_of thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
    1.17  
    1.18 +
    1.19 +(** meta data **)
    1.20 +
    1.21 +type authors = string list; (* no more for thm, rls, rew_ord, cal *)
    1.22 +type metadata = {coursedesign: authors, mathauthors: authors}
    1.23 +(*WAS IN Thy_Write:  datatype thydata
    1.24 +    = ...
    1.25 +    | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}*)
    1.26 +val default_metadata = {coursedesign = ["(c) isac team 2006"], mathauthors = []}
    1.27 +
    1.28 +structure Data = Theory_Data
    1.29 +(
    1.30 +  type T = metadata option;
    1.31 +  val empty = SOME default_metadata;
    1.32 +  fun merge _ = NONE;
    1.33 +);
    1.34 +val the_metadata = the o Data.get;
    1.35 +val set_metadata = Data.put o SOME;
    1.36 +
    1.37 +
    1.38  (**)end(**)

     2.1 --- a/src/Tools/isac/Interpret/Interpret.thy	Fri Jan 06 09:55:35 2023 +0100
     2.2 +++ b/src/Tools/isac/Interpret/Interpret.thy	Fri Jan 06 10:33:16 2023 +0100
     2.3 @@ -29,33 +29,6 @@
     2.4      if isac_names_known_sofar = ThyC.session_interpret_names @ ThyC.session_specify_names then ()
     2.5      else raise ERROR "theory dependencies not as anticipated in ThyC"
     2.6  end
     2.7 -\<close> ML \<open> (*\------------------------------------ keep ------------------------------------------/*)
     2.8 -\<close> text \<open> (* error in Integrate, EqSystem *)
     2.9 -open ThyC (* <---------------------------------------------------------------------------------*)
    2.10 -
    2.11 -  type authors = string list; (* no more for thm, rls, rew_ord, cal *)
    2.12 -  type metadata = {coursedesign: authors, html: string, mathauthors: authors}
    2.13 -(*WAS IN Thy_Write:  datatype thydata
    2.14 -    = ...
    2.15 -    | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}*)
    2.16 -
    2.17 -  structure Data = Theory_Data
    2.18 -  (
    2.19 -    type T = metadata option;
    2.20 -    val empty = NONE;  (*####### TODO: Htmldefault mit 2006 nehmen ############################*)
    2.21 -    fun merge _ = NONE;
    2.22 -  );
    2.23 -  val the_metadata = the o Data.get;
    2.24 -  val set_metadata = Data.put o SOME;
    2.25 -
    2.26 -the_metadata: theory -> metadata;
    2.27 -set_metadata: metadata -> theory -> theory;
    2.28 -\<close> text \<open>
    2.29 -open Error_Pattern (* <------------------------------------------------------------------------*)
    2.30 -\<close> ML \<open>
    2.31 -\<close> text \<open> (*Pbl_Met_Hierarchy.update_metpair  WITHIN  Know_Store.add_mets  AS MODEL*)
    2.32 -fun insert_in_method thy metID errpats = 123
    2.33 -
    2.34  \<close> ML \<open>
    2.35  \<close> ML \<open>
    2.36  \<close>

     3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Fri Jan 06 09:55:35 2023 +0100
     3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Fri Jan 06 10:33:16 2023 +0100
     3.3 @@ -76,7 +76,11 @@
     3.4  
     3.5  section \<open>Acknowledgements shown in browsers of Isac_Knowledge\<close>
     3.6  
     3.7 -(* there will be other ways in Isabelle/PIDE * )
     3.8 +setup \<open>ThyC.set_metadata {
     3.9 +  coursedesign = ["(c) Christian Dürnsteiner 2006 supported by a grant from NMI Austria"],
    3.10 +  mathauthors = ["Walther Neuper 2005 supported by a grant from NMI Austria"]}
    3.11 +\<close>
    3.12 +(* ? more finegrained as above in Isabelle/PIDE ?* )
    3.13  setup \<open>
    3.14  Know_Store.add_thes
    3.15    [Thy_Hierarchy.make_thy @{theory}