1.1 --- a/src/Tools/isac/calcelems.sml Tue Feb 06 16:59:09 2018 +0100
1.2 +++ b/src/Tools/isac/calcelems.sml Wed Feb 07 10:24:16 2018 +0100
1.3 @@ -237,6 +237,10 @@
1.4 type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
1.5 type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
1.6 type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
1.7 +
1.8 +(* Since Isabelle2017 sessions in theory identifiers are enforced.
1.9 + However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
1.10 +fun Thy_Info_get_theory thyID = Thy_Info_get_theory ("Isac." ^ thyID)
1.11
1.12 fun term_to_string' ctxt t =
1.13 let
1.14 @@ -244,14 +248,14 @@
1.15 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.16 fun term_to_string'' (thyID : thyID) t =
1.17 let
1.18 - val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
1.19 + val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
1.20 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.21 fun term_to_string''' thy t =
1.22 let
1.23 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
1.24 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.25
1.26 -fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info.get_theory thy');(*FIXXXME thy-ctxt*)
1.27 +fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*)
1.28 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
1.29
1.30 fun term2str t = term_to_string' (thy2ctxt' "Isac") t;
1.31 @@ -271,7 +275,7 @@
1.32 in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
1.33 fun type_to_string'' (thyID : thyID) t =
1.34 let
1.35 - val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
1.36 + val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
1.37 in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
1.38 fun type_to_string''' thy t =
1.39 let
1.40 @@ -369,7 +373,7 @@
1.41 val theory2theory' = string_of_thy;
1.42 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
1.43 val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy;
1.44 -(* fun theory'2theory = fun thyID2thy ... see fun assoc_thy (...Thy_Info.get_theory string);
1.45 +(* fun theory'2theory = fun thyID2thy ... see fun assoc_thy (...Thy_Info_get_theory string);
1.46 al it = "Isac" : string
1.47 *)
1.48
1.49 @@ -421,7 +425,7 @@
1.50 and interactively specifiying thys in subpbl is not very relevant.
1.51
1.52 Other solutions possible:
1.53 - # always parse and type-check with Thy_Info.get_theory "Isac"
1.54 + # always parse and type-check with Thy_Info_get_theory "Isac"
1.55 (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
1.56 # regard the subthy-relation in specifying thys of subpbls
1.57 # specifically handle 'SubProblem (undefined, pbl, arglist)'
1.58 @@ -784,8 +788,8 @@
1.59 if key = keyi then SOME xi else assoc' (pairs, key);
1.60
1.61 fun assoc_thy (thy:theory') =
1.62 - if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*)
1.63 - else (Thy_Info.get_theory thy)
1.64 + if thy = "e_domID" then (Thy_Info_get_theory "Script") (*lower bound of Knowledge*)
1.65 + else (Thy_Info_get_theory thy)
1.66 handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
1.67
1.68 (*.overwrite an element in an association list and pair it with a thyID
1.69 @@ -1088,24 +1092,24 @@
1.70 section "Get and group the theories defined in Isac" *)
1.71 fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*)
1.72 let
1.73 - val allthys = Theory.ancestors_of (Thy_Info.get_theory "Build_Thydata")
1.74 + val allthys = Theory.ancestors_of (Thy_Info_get_theory "Build_Thydata")
1.75 in
1.76 - drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys)
1.77 + drop ((find_index (curry Context.eq_thy (Thy_Info_get_theory "Complex_Main")) allthys), allthys)
1.78 end
1.79 fun knowthys () = (*["Isac", .., "Descript", "Delete"]*)
1.80 let
1.81 fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
1.82 let
1.83 val allthys = filter_out (member Context.eq_thy
1.84 - [(*Thy_Info.get_theory "ProgLang",*) Thy_Info.get_theory "Interpret",
1.85 - Thy_Info.get_theory "xmlsrc", Thy_Info.get_theory "Frontend"])
1.86 - (Theory.ancestors_of (Thy_Info.get_theory "Build_Thydata"))
1.87 + [(*Thy_Info_get_theory "ProgLang",*) Thy_Info_get_theory "Interpret",
1.88 + Thy_Info_get_theory "xmlsrc", Thy_Info_get_theory "Frontend"])
1.89 + (Theory.ancestors_of (Thy_Info_get_theory "Build_Thydata"))
1.90 in
1.91 - take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
1.92 + take ((find_index (curry Context.eq_thy (Thy_Info_get_theory "Complex_Main")) allthys),
1.93 allthys)
1.94 end
1.95 val isacthys' = isacthys ()
1.96 - val proglang_parent = Thy_Info.get_theory "ProgLang"
1.97 + val proglang_parent = Thy_Info_get_theory "ProgLang"
1.98 in
1.99 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')
1.100 end
1.101 @@ -1114,15 +1118,15 @@
1.102 fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
1.103 let
1.104 val allthys = filter_out (member Context.eq_thy
1.105 - [(*Thy_Info.get_theory "ProgLang",*) Thy_Info.get_theory "Interpret",
1.106 - Thy_Info.get_theory "xmlsrc", Thy_Info.get_theory "Frontend"])
1.107 - (Theory.ancestors_of (Thy_Info.get_theory "Build_Thydata"))
1.108 + [(*Thy_Info_get_theory "ProgLang",*) Thy_Info_get_theory "Interpret",
1.109 + Thy_Info_get_theory "xmlsrc", Thy_Info_get_theory "Frontend"])
1.110 + (Theory.ancestors_of (Thy_Info_get_theory "Build_Thydata"))
1.111 in
1.112 - take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
1.113 + take ((find_index (curry Context.eq_thy (Thy_Info_get_theory "Complex_Main")) allthys),
1.114 allthys)
1.115 end
1.116 val isacthys' = isacthys ()
1.117 - val proglang_parent = Thy_Info.get_theory "ProgLang"
1.118 + val proglang_parent = Thy_Info_get_theory "ProgLang"
1.119 in
1.120 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
1.121 end
1.122 @@ -1132,7 +1136,7 @@
1.123 else if member Context.eq_thy (progthys ()) thy then "IsacScripts"
1.124 else if member Context.eq_thy (isabthys ()) thy then "Isabelle"
1.125 else error ("closure of thys in Isac is broken by " ^ string_of_thy thy)
1.126 -fun partID' (thy' : theory') = partID (Thy_Info.get_theory thy')
1.127 +fun partID' (thy' : theory') = partID (Thy_Info_get_theory thy')
1.128 (*
1.129 end (*struct*)
1.130 *)