16 |
16 |
17 val maxthy: theory -> theory -> theory |
17 val maxthy: theory -> theory -> theory |
18 |
18 |
19 type pbt_ = string * (term * term) |
19 type pbt_ = string * (term * term) |
20 val update_hrls: Thy_Html.thydata -> Error_Pattern_Def.id list -> Thy_Html.thydata |
20 val update_hrls: Thy_Html.thydata -> Error_Pattern_Def.id list -> Thy_Html.thydata |
21 |
|
22 (*/------- to ? from Celem -------\*) |
|
23 val knowthys: unit -> theory list |
|
24 val isabthys: unit -> theory list |
|
25 val partID': ThyC.id -> string |
|
26 (*\------- to ? from Celem -------/*) |
|
27 |
21 |
28 end |
22 end |
29 |
23 |
30 (**) |
24 (**) |
31 structure Celem(**): CALC_ELEMENT(**) = |
25 structure Celem(**): CALC_ELEMENT(**) = |
63 Thy_Html.Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors, |
57 Thy_Html.Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors, |
64 thy_rls = (thyID, rls')} |
58 thy_rls = (thyID, rls')} |
65 end |
59 end |
66 | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments"; |
60 | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments"; |
67 |
61 |
68 |
|
69 (*/------- to ? from Celem -------\*) |
|
70 (* group the theories defined in Isac, compare Build_Thydata: |
|
71 section "Get and group the theories defined in Isac" *) |
|
72 fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*) |
|
73 let |
|
74 val allthys = Theory.ancestors_of (ThyC.get_theory "Build_Thydata") |
|
75 in |
|
76 drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys) |
|
77 end |
|
78 fun knowthys () = (*["Isac_Knowledge", .., "Descript"]*) |
|
79 let |
|
80 fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *) |
|
81 let |
|
82 val allthys = filter_out (member Context.eq_thy |
|
83 [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret", |
|
84 ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"]) |
|
85 (Theory.ancestors_of (ThyC.get_theory "Build_Thydata")) |
|
86 in |
|
87 take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), |
|
88 allthys) |
|
89 end |
|
90 val isacthys' = isacthys () |
|
91 val proglang_parent = ThyC.get_theory "ProgLang" |
|
92 in |
|
93 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys') |
|
94 end |
|
95 fun progthys () = (*["Isac_Knowledge", .., "Descript"]*) |
|
96 let |
|
97 fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *) |
|
98 let |
|
99 val allthys = filter_out (member Context.eq_thy |
|
100 [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret", |
|
101 ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"]) |
|
102 (Theory.ancestors_of (ThyC.get_theory "Build_Thydata")) |
|
103 in |
|
104 take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), |
|
105 allthys) |
|
106 end |
|
107 val isacthys' = isacthys () |
|
108 val proglang_parent = ThyC.get_theory "ProgLang" |
|
109 in |
|
110 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys') |
|
111 end |
|
112 fun partID thy = |
|
113 if member Context.eq_thy (knowthys ()) thy then "IsacKnowledge" |
|
114 else if member Context.eq_thy (progthys ()) thy then "IsacScripts" |
|
115 else if member Context.eq_thy (isabthys ()) thy then "Isabelle" |
|
116 else error ("closure of thys in Isac is broken by " ^ Context.theory_name thy) |
|
117 fun partID' thy' = partID (ThyC.get_theory thy') |
|
118 (*\------- to ? from Celem -------/*) |
|
119 |
|
120 end (*struct*) |
62 end (*struct*) |
121 |
63 |