prep. purge code for libisabelle
1.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Wed Apr 21 11:47:33 2021 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Thu Apr 22 12:49:13 2021 +0200
1.3 @@ -1,6 +1,9 @@
1.4 (* Title: collect all defitions for xml generation and libisabelle (Las Hupel)
1.5 Author: Walther Neuper 110226
1.6 (c) due to copyright terms
1.7 +
1.8 +Since libisabelle has been discontinued, this directory will disappear eventually.
1.9 +Remaining code will be located elsewhere.
1.10 *)
1.11
1.12 theory BridgeLibisabelle
1.13 @@ -17,7 +20,15 @@
1.14
1.15 ML \<open>
1.16 \<close> ML \<open>
1.17 +(*
1.18 + The only code kept for generation of XML (required by Isac's old Java frontend)
1.19 + is called below.
1.20 + The hierarchies below will still be required in addition to PIDE functionality.
1.21 +*)
1.22 +val path = "/home/wneuper/tmp/"; (*~/tmp/pbl/ and ~/tmp/met must be created manyally*)
1.23 \<close> ML \<open>
1.24 +Pbl_Met_Hierarchy.pbl_hierarchy2file (path ^ "pbl/");
1.25 +Pbl_Met_Hierarchy.met_hierarchy2file (path ^ "met/");
1.26 \<close> ML \<open>
1.27 \<close>
1.28 -end
1.29 \ No newline at end of file
1.30 +end
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 21 11:47:33 2021 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Thu Apr 22 12:49:13 2021 +0200
2.3 @@ -1,12 +1,9 @@
2.4 -(* the interface between the isac-kernel and the java-frontend;
2.5 - the isac-kernel holds calc-trees; stdout in XML-format.
2.6 - This is the only file which does not adhere to Isabelle coding standards,
2.7 - rather the function names are according to the respective Java methods.
2.8 +(* Interface between the isac-kernel and the java-frontend;
2.9 authors: Walther Neuper 2002
2.10 (c) due to copyright terms
2.11
2.12 -use"Frontend/interface.sml";
2.13 -use"interface.sml";
2.14 + This interface is being replaced by Isabelle/PIDE, but still remains
2.15 + as long as many tests imitate interaction via libisabelle.
2.16 *)
2.17
2.18 signature KERNEL =
3.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 21 11:47:33 2021 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Thu Apr 22 12:49:13 2021 +0200
3.3 @@ -313,8 +313,12 @@
3.4 fun pbls2file path = nodes path [] [0] pbl2file (get_ptyps ());
3.5 fun mets2file path = nodes path [] [0] met2file (get_mets ());
3.6 (*
3.7 -val path = "/home/neuper/proto2/isac/xmldata/";
3.8 -val path = "/home/neuper/tmp/";
3.9 +~@wneuper-w541:~/tmp$ mkdir pbl
3.10 +~@wneuper-w541:~/tmp$ mkdir met
3.11 +~@wneuper-w541:~/tmp$ mkdir thy
3.12 +
3.13 +val path = "/home/wneuper/proto2/isac/xmldata/";
3.14 +val path = "/home/wneuper/tmp/";
3.15
3.16 pbl_hierarchy2file (path ^ "pbl/");
3.17 pbls2file (path ^ "pbl/");
4.1 --- a/src/Tools/isac/Isac_Protocol.thy Wed Apr 21 11:47:33 2021 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,724 +0,0 @@
4.4 -theory Isac_Protocol
4.5 -imports "$ISABELLE_ISAC/Knowledge/Build_Thydata" Protocol.Protocol
4.6 -begin
4.7 -
4.8 -(* val appendFormula : calcID -> cterm' -> XML.tree *)
4.9 -operation_setup (sequential, bracket, auto) append_form =
4.10 - \<open>fn intree =>
4.11 - (let
4.12 - val (calcid, cterm') = case intree of
4.13 - XML.Elem (("APPENDFORMULA", []), [
4.14 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.15 - form]) => (ci |> TermC.int_of_str, form |> xml_to_term_NEW |> UnparseC.term)
4.16 - | x => raise ERROR ("append_form: WRONG intree = " ^ xmlstr 0 x)
4.17 - val result = Kernel.appendFormula calcid cterm'
4.18 - in result end)
4.19 - handle ERROR msg => appendformulaERROR2xml 4711 msg\<close>
4.20 -
4.21 -(* val autoCalculate : calcID -> auto -> XML.tree *)
4.22 -operation_setup autocalculate = \<open>
4.23 - {from_lib = Codec.tree,
4.24 - to_lib = Codec.tree,
4.25 - action = (fn intree =>
4.26 - (let
4.27 - val (ci, a) = case intree of
4.28 - XML.Elem (("AUTOCALC", []), [
4.29 - XML.Elem (("CALCID", []), [XML.Text ci]), a]) => (ci, a)
4.30 - | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
4.31 - val SOME calcid = TermC.int_opt_of_string ci
4.32 - val auto = xml_to_auto a
4.33 - val result = Kernel.autoCalculate calcid auto
4.34 - in result end)
4.35 - handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
4.36 -
4.37 -(* val applyTactic : calcID -> pos' -> tac -> XML.tree *)
4.38 -operation_setup apply_tac = \<open>
4.39 - {from_lib = Codec.tree,
4.40 - to_lib = Codec.tree,
4.41 - action = (fn intree =>
4.42 - (let
4.43 - val (ci, pos, tac) = case intree of
4.44 - XML.Elem (("AUTOCALC", []), [
4.45 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.46 - pos, tac]) => (TermC.int_of_str ci, xml_to_pos pos, xml_to_tac tac)
4.47 - | tree => raise ERROR ("apply_tac: WRONG intree = " ^ xmlstr 0 tree)
4.48 - val result = Kernel.applyTactic ci pos tac
4.49 - in result end)
4.50 - handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
4.51 -
4.52 -(* val CalcTree : fmz list -> XML.tree *)
4.53 -operation_setup calctree = \<open>
4.54 - {from_lib = Codec.tree,
4.55 - to_lib = Codec.tree,
4.56 - action = (fn intree =>
4.57 - (let
4.58 - val fmz = case intree of
4.59 - tree as XML.Elem (("FORMALIZATION", []), vars) => xml_to_fmz tree
4.60 - | tree => raise ERROR ("calctree: WRONG intree = " ^ xmlstr 0 tree)
4.61 - val result = Kernel.CalcTree fmz
4.62 - in result end)
4.63 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.64 -
4.65 -(* val checkContext : calcID -> pos' -> guh -> XML.tree *)
4.66 -operation_setup check_ctxt = \<open>
4.67 - {from_lib = Codec.tree,
4.68 - to_lib = Codec.tree,
4.69 - action = (fn intree =>
4.70 - (let
4.71 - val (ci, pos, guh) = case intree of
4.72 - XML.Elem (("CONTEXTTHY", []), [
4.73 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.74 - pos as XML.Elem (("POSITION", []), _),
4.75 - XML.Elem (("GUH", []), [XML.Text guh])])
4.76 - => (TermC.int_of_str ci, xml_to_pos pos, guh)
4.77 - | tree => raise ERROR ("check_ctxt: WRONG intree = " ^ xmlstr 0 tree)
4.78 - val result = Kernel.checkContext ci pos guh
4.79 - in result end)
4.80 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.81 -
4.82 -(* val DEconstrCalcTree : calcID -> XML.tree *)
4.83 -operation_setup deconstrcalctree = \<open>
4.84 - {from_lib = Codec.int,
4.85 - to_lib = Codec.tree,
4.86 - action = (fn calcid =>
4.87 - let
4.88 - val result = Kernel.DEconstrCalcTree calcid
4.89 - in result end)}\<close>
4.90 -
4.91 -(* val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree *)
4.92 -operation_setup fetch_applicable_tacs = \<open>
4.93 - {from_lib = Codec.tree,
4.94 - to_lib = Codec.tree,
4.95 - action = (fn intree =>
4.96 - (let
4.97 - val (ci, i, pos) = case intree of
4.98 - XML.Elem (("APPLICABLETACTICS", []), [
4.99 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.100 - XML.Elem (("INT", []), [XML.Text i]),
4.101 - pos as XML.Elem (("POSITION", []), _)])
4.102 - => (TermC.int_of_str ci, TermC.int_of_str i, xml_to_pos pos)
4.103 - | tree => raise ERROR ("fetch_applicable_tacs: WRONG intree = " ^ xmlstr 0 tree)
4.104 - val result = Kernel.fetchApplicableTactics ci i pos
4.105 - in result end)
4.106 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.107 -
4.108 -(* val fetchProposedTactic : calcID -> XML.tree *)
4.109 -operation_setup fetch_proposed_tac = \<open>
4.110 - {from_lib = Codec.tree,
4.111 - to_lib = Codec.tree,
4.112 - action = (fn intree =>
4.113 - (let
4.114 - val (ci) = case intree of
4.115 - XML.Elem (("NEXTTAC", []), [
4.116 - XML.Elem (("CALCID", []), [XML.Text ci])]) => (TermC.int_of_str ci)
4.117 - | tree => raise ERROR ("fetch_proposed_tac: WRONG intree = " ^ xmlstr 0 tree)
4.118 - val result = Kernel.fetchProposedTactic ci
4.119 - in result end)
4.120 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.121 -
4.122 -(* val findFillpatterns : calcID -> errpatID -> XML.tree *)
4.123 -operation_setup find_fill_patts = \<open>
4.124 - {from_lib = Codec.tree,
4.125 - to_lib = Codec.tree,
4.126 - action = (fn intree =>
4.127 - (let
4.128 - val (ci, err_pat_id) = case intree of
4.129 - XML.Elem (("FINDFILLPATTERNS", []), [
4.130 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.131 - XML.Elem (("STRING", []), [XML.Text err_pat_id])])
4.132 - => (TermC.int_of_str ci, err_pat_id)
4.133 - | tree => raise ERROR ("find_fill_patts: WRONG intree = " ^ xmlstr 0 tree)
4.134 - val result = Kernel.findFillpatterns ci err_pat_id
4.135 - in result end)
4.136 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.137 -
4.138 -(* val getAccumulatedAsms : calcID -> pos' -> XML.tree *)
4.139 -operation_setup get_accumulated_asms = \<open>
4.140 - {from_lib = Codec.tree,
4.141 - to_lib = Codec.tree,
4.142 - action = (fn intree =>
4.143 - (let
4.144 - val (ci, pos) = case intree of
4.145 - XML.Elem (("GETASSUMPTIONS", []), [
4.146 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.147 - pos as XML.Elem (("POSITION", []), _)])
4.148 - => (TermC.int_of_str ci, xml_to_pos pos)
4.149 - | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
4.150 - val result = Kernel.getAccumulatedAsms ci pos
4.151 - in result end)
4.152 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.153 -
4.154 -(* val getActiveFormula : calcID -> XML.tree *)
4.155 -operation_setup get_active_form = \<open>
4.156 - {from_lib = Codec.tree,
4.157 - to_lib = Codec.tree,
4.158 - action = (fn intree =>
4.159 - (let
4.160 - val (ci) = case intree of
4.161 - XML.Elem (("CALCITERATOR", []), [
4.162 - XML.Elem (("CALCID", []), [XML.Text ci])])
4.163 - => (TermC.int_of_str ci)
4.164 - | tree => raise ERROR ("get_active_form: WRONG intree = " ^ xmlstr 0 tree)
4.165 - val result = Kernel.getActiveFormula ci
4.166 - in result end)
4.167 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.168 -
4.169 -(* val getAssumptions : calcID -> pos' -> XML.tree *)
4.170 -operation_setup get_asms = \<open>
4.171 - {from_lib = Codec.tree,
4.172 - to_lib = Codec.tree,
4.173 - action = (fn intree =>
4.174 - (let
4.175 - val (ci, pos) = case intree of
4.176 - XML.Elem (("APPLICABLETACTICS", []), [
4.177 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.178 - pos as XML.Elem (("POSITION", []), _)])
4.179 - => (TermC.int_of_str ci, xml_to_pos pos)
4.180 - | tree => raise ERROR ("get_asms: WRONG intree = " ^ xmlstr 0 tree)
4.181 - val result = Kernel.getAssumptions ci pos
4.182 - in result end)
4.183 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.184 -
4.185 -(* val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree *)
4.186 -operation_setup getformulaefromto = \<open>
4.187 - {from_lib = Codec.tree,
4.188 - to_lib = Codec.tree,
4.189 - action = (fn intree =>
4.190 - (let
4.191 - val (calcid, from, to, level, rules) = case intree of
4.192 - XML.Elem (("GETFORMULAEFROMTO", []), [
4.193 - XML.Elem (("CALCID", []), [XML.Text calcid]),
4.194 - from as XML.Elem (("POSITION", []), [
4.195 - XML.Elem (("INTLIST", []), _),
4.196 - XML.Elem (("POS", []), [XML.Text _])]),
4.197 - to as XML.Elem (("POSITION", []), [
4.198 - XML.Elem (("INTLIST", []), _),
4.199 - XML.Elem (("POS", []), [XML.Text _])]),
4.200 - XML.Elem (("INT", []), [XML.Text level]),
4.201 - XML.Elem (("BOOL", []), [XML.Text rules])])
4.202 - => (TermC.int_of_str calcid, xml_to_pos from, xml_to_pos to, TermC.int_of_str level, string_to_bool rules)
4.203 - | tree => raise ERROR ("getformulaefromto: WRONG intree = " ^ xmlstr 0 tree)
4.204 - val result = Kernel.getFormulaeFromTo calcid from to level rules
4.205 - in result end)
4.206 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.207 -
4.208 -(* val getTactic : calcID -> pos' -> XML.tree *)
4.209 -operation_setup get_tac = \<open>
4.210 - {from_lib = Codec.tree,
4.211 - to_lib = Codec.tree,
4.212 - action = (fn intree =>
4.213 - (let
4.214 - val (ci, pos) = case intree of
4.215 - XML.Elem (("GETTACTIC", []), [
4.216 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.217 - pos as XML.Elem (("POSITION", []), _)])
4.218 - => (TermC.int_of_str ci, xml_to_pos pos)
4.219 - | tree => raise ERROR ("get_tac: WRONG intree = " ^ xmlstr 0 tree)
4.220 - val result = Kernel.getTactic ci pos
4.221 - in result end)
4.222 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.223 -
4.224 -(* val initContext : calcID -> ketype -> pos' -> XML.tree *)
4.225 -operation_setup init_ctxt = \<open>
4.226 - {from_lib = Codec.tree,
4.227 - to_lib = Codec.tree,
4.228 - action = (fn intree =>
4.229 - ((let
4.230 - val (ci, ketype, pos) = case intree of
4.231 - XML.Elem (("INITCONTEXT", []), [
4.232 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.233 - ketype as XML.Elem (("KETYPE", []), _),
4.234 - pos as XML.Elem (("POSITION", []), _)])
4.235 - => (TermC.int_of_str ci, xml_to_ketype ketype, xml_to_pos pos)
4.236 - | tree => raise ERROR ("init_ctxt: WRONG intree = " ^ xmlstr 0 tree)
4.237 - val result = Kernel.initContext ci ketype pos
4.238 - in result end)
4.239 - handle ERROR msg => sysERROR2xml 4711 msg)
4.240 - handle _ => sysERROR2xml 4711 "Protocol.operation_setup init_ctxt UNKNOWN exn")}\<close>
4.241 -
4.242 -(* val inputFillFormula: calcID -> string -> XML.tree *)
4.243 -operation_setup input_fill_form = \<open>
4.244 - {from_lib = Codec.tree,
4.245 - to_lib = Codec.tree,
4.246 - action = (fn intree =>
4.247 - (let
4.248 - val (ci, str) = case intree of
4.249 - XML.Elem (("AUTOCALC", []), [
4.250 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.251 - XML.Elem (("STRING", []), [XML.Text str])])
4.252 - => (TermC.int_of_str ci, str)
4.253 - | tree => raise ERROR ("input_fill_form: WRONG intree = " ^ xmlstr 0 tree)
4.254 - val result = Kernel.inputFillFormula ci str
4.255 - in result end)
4.256 - handle ERROR msg => message2xml 4711 msg)}\<close>
4.257 -
4.258 -(* val interSteps : calcID -> pos' -> XML.tree *)
4.259 -operation_setup inter_steps = \<open>
4.260 - {from_lib = Codec.tree,
4.261 - to_lib = Codec.tree,
4.262 - action = (fn intree =>
4.263 - (let
4.264 - val (ci, pos) = case intree of
4.265 - XML.Elem (("INTERSTEPS", []), [
4.266 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.267 - pos as XML.Elem (("POSITION", []), _)])
4.268 - => (TermC.int_of_str ci, xml_to_pos pos)
4.269 - | tree => raise ERROR ("inter_steps: WRONG intree = " ^ xmlstr 0 tree)
4.270 - val result = Kernel.interSteps ci pos
4.271 - in result end)
4.272 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.273 -
4.274 -(* val Iterator : calcID -> XML.tree *)
4.275 -operation_setup iterator = \<open>
4.276 - {from_lib = Codec.int,
4.277 - to_lib = Codec.tree,
4.278 - action = (fn calcid =>
4.279 - let
4.280 - val result = Kernel.Iterator calcid
4.281 - in result end)}\<close>
4.282 -
4.283 -(* val IteratorTEST : calcID -> iterID *)
4.284 -
4.285 -(* val modelProblem : calcID -> XML.tree *)
4.286 -operation_setup model_pbl = \<open>
4.287 - {from_lib = Codec.tree,
4.288 - to_lib = Codec.tree,
4.289 - action = (fn intree =>
4.290 - (let
4.291 - val (ci) = case intree of
4.292 - XML.Elem (("MODIFYCALCHEAD", []), [
4.293 - XML.Elem (("CALCID", []), [XML.Text ci])])
4.294 - => (TermC.int_of_str ci)
4.295 - | tree => raise ERROR ("model_pbl: WRONG intree = " ^ xmlstr 0 tree)
4.296 - val result = Kernel.modelProblem ci
4.297 - in result end)
4.298 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.299 -
4.300 -(* val modifyCalcHead : calcID -> icalhd -> XML.tree *)
4.301 -operation_setup modify_calchead = \<open>
4.302 - {from_lib = Codec.tree,
4.303 - to_lib = Codec.tree,
4.304 - action = (fn intree =>
4.305 - (let
4.306 - val (ci, icalhd) = case intree of
4.307 - XML.Elem (("MODIFYCALCHEAD", []), [
4.308 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.309 - icalhd])
4.310 - => (TermC.int_of_str ci, xml_to_icalhd icalhd)
4.311 - | tree => raise ERROR ("modify_calchead: WRONG intree = " ^ xmlstr 0 tree)
4.312 - val result = Kernel.modifyCalcHead ci icalhd
4.313 - in result end)
4.314 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.315 -
4.316 -(* val moveActiveCalcHead : calcID -> XML.tree *)
4.317 -operation_setup move_active_calchead = \<open>
4.318 - {from_lib = Codec.tree,
4.319 - to_lib = Codec.tree,
4.320 - action = (fn intree =>
4.321 - (let
4.322 - val (ci) = case intree of
4.323 - XML.Elem (("CALCITERATOR", []), [
4.324 - XML.Elem (("CALCID", []), [XML.Text ci])])
4.325 - => (TermC.int_of_str ci)
4.326 - | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
4.327 - val result = Kernel.moveActiveCalcHead ci
4.328 - in result end)
4.329 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.330 -
4.331 -(* val moveActiveDown : calcID -> XML.tree *)
4.332 -operation_setup move_active_down = \<open>
4.333 - {from_lib = Codec.tree,
4.334 - to_lib = Codec.tree,
4.335 - action = (fn intree =>
4.336 - (let
4.337 - val (ci) = case intree of
4.338 - XML.Elem (("CALCITERATOR", []), [
4.339 - XML.Elem (("CALCID", []), [XML.Text ci])])
4.340 - => (TermC.int_of_str ci)
4.341 - | tree => raise ERROR ("move_active_down: WRONG intree = " ^ xmlstr 0 tree)
4.342 - val result = Kernel.moveActiveDown ci
4.343 - in result end)
4.344 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.345 -
4.346 -(* val moveActiveFormula : calcID -> pos' -> XML.tree *)
4.347 -operation_setup move_active_form = \<open>
4.348 - {from_lib = Codec.tree,
4.349 - to_lib = Codec.tree,
4.350 - action = (fn intree =>
4.351 - (let
4.352 - val (ci, pos) = case intree of
4.353 - XML.Elem (("CALCITERATOR", []), [
4.354 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.355 - pos as XML.Elem (("POSITION", []), _)])
4.356 - => (TermC.int_of_str ci, xml_to_pos pos)
4.357 - | tree => raise ERROR ("move_active_form: WRONG intree = " ^ xmlstr 0 tree)
4.358 - val result = Kernel.moveActiveFormula ci pos
4.359 - in result end)
4.360 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.361 -
4.362 -(* val moveActiveLevelDown : calcID -> XML.tree *)
4.363 -operation_setup move_active_levdown = \<open>
4.364 - {from_lib = Codec.tree,
4.365 - to_lib = Codec.tree,
4.366 - action = (fn intree =>
4.367 - (let
4.368 - val (ci) = case intree of
4.369 - XML.Elem (("CALCITERATOR", []), [
4.370 - XML.Elem (("CALCID", []), [XML.Text ci])])
4.371 - => (TermC.int_of_str ci)
4.372 - | tree => raise ERROR ("move_active_levdown: WRONG intree = " ^ xmlstr 0 tree)
4.373 - val result = Kernel.moveActiveLevelDown ci
4.374 - in result end)
4.375 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.376 -
4.377 -(* val moveActiveLevelUp : calcID -> XML.tree *)
4.378 -operation_setup move_active_levup = \<open>
4.379 - {from_lib = Codec.tree,
4.380 - to_lib = Codec.tree,
4.381 - action = (fn intree =>
4.382 - (let
4.383 - val (ci) = case intree of
4.384 - XML.Elem (("CALCITERATOR", []), [
4.385 - XML.Elem (("CALCID", []), [XML.Text ci])])
4.386 - => (TermC.int_of_str ci)
4.387 - | tree => raise ERROR ("move_active_levup: WRONG intree = " ^ xmlstr 0 tree)
4.388 - val result = Kernel.moveActiveLevelUp ci
4.389 - in result end)
4.390 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.391 -
4.392 -(* val moveActiveRoot : calcID -> XML.tree *)
4.393 -operation_setup moveactiveroot = \<open>
4.394 - {from_lib = Codec.int,
4.395 - to_lib = Codec.tree,
4.396 - action = (fn calcid =>
4.397 - let
4.398 - val result = Kernel.moveActiveRoot calcid
4.399 - in result end)}\<close>
4.400 -
4.401 -(* val moveActiveRootTEST : calcID -> XML.tree *)
4.402 -
4.403 -(* val moveActiveUp : calcID -> XML.tree *)
4.404 -operation_setup move_active_up = \<open>
4.405 - {from_lib = Codec.tree,
4.406 - to_lib = Codec.tree,
4.407 - action = (fn intree =>
4.408 - (let
4.409 - val (ci) = case intree of
4.410 - XML.Elem (("CALCITERATOR", []), [
4.411 - XML.Elem (("CALCID", []), [XML.Text ci])])
4.412 - => (TermC.int_of_str ci)
4.413 - | tree => raise ERROR ("move_active_up: WRONG intree = " ^ xmlstr 0 tree)
4.414 - val result = Kernel.moveActiveUp ci
4.415 - in result end)
4.416 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.417 -
4.418 -(* val moveCalcHead : calcID -> pos' -> XML.tree *)
4.419 -operation_setup move_calchead = \<open>
4.420 - {from_lib = Codec.tree,
4.421 - to_lib = Codec.tree,
4.422 - action = (fn intree =>
4.423 - (let
4.424 - val (ci, pos) = case intree of
4.425 - XML.Elem (("CALCITERATOR", []), [
4.426 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.427 - pos as XML.Elem (("POSITION", []), _)])
4.428 - => (TermC.int_of_str ci, xml_to_pos pos)
4.429 - | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
4.430 - val result = Kernel.moveCalcHead ci pos
4.431 - in result end)
4.432 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.433 -
4.434 -(* val moveDown : calcID -> pos' -> XML.tree *)
4.435 -operation_setup move_down = \<open>
4.436 - {from_lib = Codec.tree,
4.437 - to_lib = Codec.tree,
4.438 - action = (fn intree =>
4.439 - (let
4.440 - val (ci, pos) = case intree of
4.441 - XML.Elem (("CALCITERATOR", []), [
4.442 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.443 - pos as XML.Elem (("POSITION", []), _)])
4.444 - => (TermC.int_of_str ci, xml_to_pos pos)
4.445 - | tree => raise ERROR ("move_down: WRONG intree = " ^ xmlstr 0 tree)
4.446 - val result = Kernel.moveDown ci pos
4.447 - in result end)
4.448 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.449 -
4.450 -(* val moveLevelDown : calcID -> pos' -> XML.tree *)
4.451 -operation_setup move_levdn = \<open>
4.452 - {from_lib = Codec.tree,
4.453 - to_lib = Codec.tree,
4.454 - action = (fn intree =>
4.455 - (let
4.456 - val (ci, pos) = case intree of
4.457 - XML.Elem (("CALCITERATOR", []), [
4.458 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.459 - pos as XML.Elem (("POSITION", []), _)])
4.460 - => (TermC.int_of_str ci, xml_to_pos pos)
4.461 - | tree => raise ERROR ("move_levdn: WRONG intree = " ^ xmlstr 0 tree)
4.462 - val result = Kernel.moveLevelDown ci pos
4.463 - in result end)
4.464 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.465 -
4.466 -(* val moveLevelUp : calcID -> pos' -> XML.tree *)
4.467 -operation_setup move_levup = \<open>
4.468 - {from_lib = Codec.tree,
4.469 - to_lib = Codec.tree,
4.470 - action = (fn intree =>
4.471 - (let
4.472 - val (ci, pos) = case intree of
4.473 - XML.Elem (("CALCITERATOR", []), [
4.474 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.475 - pos as XML.Elem (("POSITION", []), _)])
4.476 - => (TermC.int_of_str ci, xml_to_pos pos)
4.477 - | tree => raise ERROR ("move_levup: WRONG intree = " ^ xmlstr 0 tree)
4.478 - val result = Kernel.moveLevelUp ci pos
4.479 - in result end)
4.480 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.481 -
4.482 -(* val moveRoot : calcID -> XML.tree *)
4.483 -operation_setup move_root = \<open>
4.484 - {from_lib = Codec.tree,
4.485 - to_lib = Codec.tree,
4.486 - action = (fn intree =>
4.487 - (let
4.488 - val (ci) = case intree of
4.489 - XML.Elem (("CALCITERATOR", []), [
4.490 - XML.Elem (("CALCID", []), [XML.Text ci])])
4.491 - => (TermC.int_of_str ci)
4.492 - | tree => raise ERROR ("move_root: WRONG intree = " ^ xmlstr 0 tree)
4.493 - val result = Kernel.moveRoot ci
4.494 - in result end)
4.495 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.496 -
4.497 -(* val moveUp : calcID -> pos' -> XML.tree *)
4.498 -operation_setup move_up = \<open>
4.499 - {from_lib = Codec.tree,
4.500 - to_lib = Codec.tree,
4.501 - action = (fn intree =>
4.502 - (let
4.503 - val (ci, pos) = case intree of
4.504 - XML.Elem (("CALCITERATOR", []), [
4.505 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.506 - pos as XML.Elem (("POSITION", []), _)])
4.507 - => (TermC.int_of_str ci, xml_to_pos pos)
4.508 - | tree => raise ERROR ("move_up: WRONG intree = " ^ xmlstr 0 tree)
4.509 - val result = Kernel.moveUp ci pos
4.510 - in result end)
4.511 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.512 -
4.513 -(* val refFormula : calcID -> pos' -> XML.tree *)
4.514 -operation_setup refformula = \<open>
4.515 - {from_lib = Codec.tree,
4.516 - to_lib = Codec.tree,
4.517 - action = (fn intree =>
4.518 - (let
4.519 - val (ci, p) = case intree of
4.520 - XML.Elem (("REFFORMULA", []), [
4.521 - XML.Elem (("CALCID", []), [XML.Text ci]), p])
4.522 - => (ci, p)
4.523 - | tree => raise ERROR ("refformula: WRONG intree = " ^ xmlstr 0 tree)
4.524 - val SOME calcid = TermC.int_opt_of_string ci
4.525 - val pos = xml_to_pos p
4.526 - val result = Kernel.refFormula calcid pos
4.527 - in result end)
4.528 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.529 -
4.530 -(* Refine.problem
4.531 - val refineProblem : calcID -> pos' -> guh -> XML.tree *)
4.532 -operation_setup refine_pbl = \<open>
4.533 - {from_lib = Codec.tree,
4.534 - to_lib = Codec.tree,
4.535 - action = (fn intree =>
4.536 - (let
4.537 - val (ci, pos, guh) = case intree of
4.538 - XML.Elem (("CONTEXTPBL", []), [
4.539 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.540 - pos as XML.Elem (("POSITION", []), _),
4.541 - XML.Elem (("GUH", []), [XML.Text guh])])
4.542 - => (TermC.int_of_str ci, xml_to_pos pos, guh)
4.543 - | tree => raise ERROR ("refine_pbl: WRONG intree = " ^ xmlstr 0 tree)
4.544 - val result = Kernel.refineProblem ci pos guh
4.545 - in result end)
4.546 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.547 -
4.548 -(* val replaceFormula : calcID -> cterm' -> XML.tree *)
4.549 -operation_setup replace_form = \<open>
4.550 - {from_lib = Codec.tree,
4.551 - to_lib = Codec.tree,
4.552 - action = (fn intree =>
4.553 - (let
4.554 - val (calcid, cterm') = case intree of
4.555 - XML.Elem (("REPLACEFORMULA", []), [
4.556 - XML.Elem (("CALCID", []), [XML.Text ci]), form])
4.557 - => (ci |> TermC.int_of_str, form |> xml_to_term_NEW |> UnparseC.term)
4.558 - | tree => raise ERROR ("replace_form: WRONG intree = " ^ xmlstr 0 tree)
4.559 - val result = Kernel.replaceFormula calcid cterm'
4.560 - in result end)
4.561 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.562 -
4.563 -(* val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree NOT IMPL. IN isac-java *)
4.564 -operation_setup request_fill_form = \<open>
4.565 - {from_lib = Codec.tree,
4.566 - to_lib = Codec.tree,
4.567 - action = (fn intree =>
4.568 - (let
4.569 - val (ci, errpat_id, fillpat_id) = case intree of
4.570 - XML.Elem (("AUTOCALC", []), [
4.571 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.572 - XML.Elem (("ERRPATTID", []), [XML.Text errpat_id]),
4.573 - XML.Elem (("FILLPATTID", []), [XML.Text fillpat_id])])
4.574 - => (TermC.int_of_str ci, errpat_id, fillpat_id)
4.575 - | tree => raise ERROR ("request_fill_form: WRONG intree = " ^ xmlstr 0 tree)
4.576 - val result = Kernel.requestFillformula ci (errpat_id, fillpat_id)
4.577 - in result end)
4.578 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.579 -
4.580 -(* val resetCalcHead : calcID -> XML.tree *)
4.581 -operation_setup reset_calchead = \<open>
4.582 - {from_lib = Codec.tree,
4.583 - to_lib = Codec.tree,
4.584 - action = (fn intree =>
4.585 - (let
4.586 - val (ci) = case intree of
4.587 - XML.Elem (("MODIFYCALCHEAD", []), [
4.588 - XML.Elem (("CALCID", []), [XML.Text ci])])
4.589 - => (TermC.int_of_str ci)
4.590 - | tree => raise ERROR ("reset_calchead: WRONG intree = " ^ xmlstr 0 tree)
4.591 - val result = Kernel.resetCalcHead ci
4.592 - in result end)
4.593 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.594 -
4.595 -(* val setContext : calcID -> pos' -> guh -> XML.tree *)
4.596 -operation_setup set_ctxt = \<open>
4.597 - {from_lib = Codec.tree,
4.598 - to_lib = Codec.tree,
4.599 - action = (fn intree =>
4.600 - (let
4.601 - val (ci, pos, guh) = case intree of
4.602 - XML.Elem (("CONTEXT", []), [
4.603 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.604 - pos as XML.Elem (("POSITION", []), _),
4.605 - XML.Elem (("GUH", []), [XML.Text guh])])
4.606 - => (TermC.int_of_str ci, xml_to_pos pos, guh)
4.607 - | tree => raise ERROR ("set_ctxt: WRONG intree = " ^ xmlstr 0 tree)
4.608 - val result = Kernel.setContext ci pos guh
4.609 - in result end)
4.610 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.611 -
4.612 -(*//===vvv TODO ================================================================\\\\\\\\\\\\\\\\*)
4.613 -
4.614 -(* val setMethod : calcID -> metID -> XML.tree *)
4.615 -operation_setup set_met = \<open>
4.616 - {from_lib = Codec.tree,
4.617 - to_lib = Codec.tree,
4.618 - action = (fn intree =>
4.619 - (let
4.620 - val (ci, met_id) = case intree of
4.621 - XML.Elem (("MODIFYCALCHEAD", []), [
4.622 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.623 - XML.Elem (("METHODID", []), [met_id])])
4.624 - => (TermC.int_of_str ci, xml_to_strs met_id)
4.625 - | tree => raise ERROR ("set_met: WRONG intree = " ^ xmlstr 0 tree)
4.626 - val result = Kernel.setMethod ci met_id
4.627 - in result end)
4.628 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.629 -
4.630 -(* val setNextTactic : calcID -> tac -> XML.tree *)
4.631 -operation_setup set_next_tac = \<open>
4.632 - {from_lib = Codec.tree,
4.633 - to_lib = Codec.tree,
4.634 - action = (fn intree =>
4.635 - (let
4.636 - val (ci, tac) = case intree of
4.637 - XML.Elem (("SETNEXTTACTIC", []), [
4.638 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.639 - tac])
4.640 - => (TermC.int_of_str ci, xml_to_tac tac)
4.641 - | tree => raise ERROR ("set_next_tac: WRONG intree = " ^ xmlstr 0 tree)
4.642 - val result = Kernel.setNextTactic ci tac
4.643 - in result end)
4.644 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.645 -
4.646 -(*\\===^^^ TODO ================================================================///////////////*)
4.647 -
4.648 -(* val setProblem : calcID -> pblID -> XML.tree *)
4.649 -operation_setup set_pbl = \<open>
4.650 - {from_lib = Codec.tree,
4.651 - to_lib = Codec.tree,
4.652 - action = (fn intree =>
4.653 - (let
4.654 - val (ci, pbl_id) = case intree of
4.655 - XML.Elem (("MODIFYCALCHEAD", []), [
4.656 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.657 - XML.Elem (("PROBLEMID", []), [pbl_id])])
4.658 - => (TermC.int_of_str ci, xml_to_strs pbl_id)
4.659 - | tree => raise ERROR ("set_pbl: WRONG intree = " ^ xmlstr 0 tree)
4.660 - val result = Kernel.setProblem ci pbl_id
4.661 - in result end)
4.662 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.663 -
4.664 -(* val setTheory : calcID -> thyID -> XML.tree *)
4.665 -operation_setup set_thy = \<open>
4.666 - {from_lib = Codec.tree,
4.667 - to_lib = Codec.tree,
4.668 - action = (fn intree =>
4.669 - (let
4.670 - val (ci, thy_id) = case intree of
4.671 - XML.Elem (("MODIFYCALCHEAD", []), [
4.672 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.673 - XML.Elem (("THEORYID", []), [XML.Text thy_id])])
4.674 - => (TermC.int_of_str ci, thy_id)
4.675 - | tree => raise ERROR ("set_thy: WRONG intree = " ^ xmlstr 0 tree)
4.676 - val result = Kernel.setTheory ci thy_id
4.677 - in result end)
4.678 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.679 -
4.680 -(* for inital java-tests/isac/bridge/TestTerm.scala *)
4.681 -operation_setup make_int = \<open>
4.682 - {from_lib = Codec.unit,
4.683 - to_lib = Codec.term,
4.684 - action = (fn _ => HOLogic.mk_number @{typ int} 3)}
4.685 -\<close>
4.686 -
4.687 -(* passes libisabelle term in both directions;
4.688 - the use of direction isac-java \<longrightarrow> Isabelle/Isac is a future design question *)
4.689 -operation_setup test_term_transfer = \<open>
4.690 - {from_lib = Codec.tree,
4.691 - to_lib = Codec.tree,
4.692 - action = (fn intree =>
4.693 - (let
4.694 - val t = case intree of
4.695 - XML.Elem (("MATHML", []), [
4.696 - XML.Elem (("ISA", []), [XML.Text _]),
4.697 - XML.Elem (("TERM", []), [xt])])
4.698 - => xt |> Codec.decode Codec.term |> Codec.the_success
4.699 - | tree => raise ERROR ("test_term_transfer: WRONG intree = " ^ xmlstr 0 tree)
4.700 - val test_out = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
4.701 - in xml_of_term_NEW test_out end)
4.702 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.703 -
4.704 -operation_setup test_term_one_way = \<open>
4.705 - {from_lib = Codec.string,
4.706 - to_lib = Codec.tree,
4.707 - action = (fn instr =>
4.708 - (let
4.709 - val t = instr |> TermC.parse @{theory} |> the |> Thm.term_of
4.710 - val test_out = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
4.711 - in xml_of_term_NEW test_out end)
4.712 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
4.713 -
4.714 -(* tool for creating libisabelle's terms *)
4.715 -operation_setup scalaterm_of_string = \<open>
4.716 - {from_lib = Codec.string,
4.717 - to_lib = Codec.tree,
4.718 - action = (fn instr =>
4.719 - (let
4.720 - val termopt = TermC.parseNEW (Proof_Context.init_global @{theory}) instr
4.721 - in
4.722 - case TermC.parseNEW (Proof_Context.init_global @{theory}) instr of
4.723 - SOME term => xml_of_term_NEW term
4.724 - | NONE => sysERROR2xml 4711 ("*** syntax ERROR in: " ^ instr)
4.725 - end))}\<close>
4.726 -
4.727 -end
4.728 \ No newline at end of file
5.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed Apr 21 11:47:33 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Thu Apr 22 12:49:13 2021 +0200
5.3 @@ -78,23 +78,23 @@
5.4
5.5 setup \<open>
5.6 KEStore_Elems.add_thes
5.7 - [make_thy @{theory}
5.8 + [Thy_Hierarchy.make_thy @{theory}
5.9 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
5.10 - make_isa @{theory} ("IsacKnowledge", "Theorems")
5.11 + Thy_Hierarchy.make_isa @{theory} ("IsacKnowledge", "Theorems")
5.12 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
5.13 - make_thm @{theory} "IsacKnowledge" ("Belastung_Querkraft", @{thm Belastung_Querkraft})
5.14 + Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("Belastung_Querkraft", @{thm Belastung_Querkraft})
5.15 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
5.16 - make_thm @{theory} "IsacKnowledge" ("Moment_Neigung", @{thm Moment_Neigung})
5.17 + Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("Moment_Neigung", @{thm Moment_Neigung})
5.18 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
5.19 - make_thm @{theory} "IsacKnowledge" ("Moment_Querkraft", @{thm Moment_Querkraft})
5.20 + Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("Moment_Querkraft", @{thm Moment_Querkraft})
5.21 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
5.22 - make_thm @{theory} "IsacKnowledge" ("Neigung_Moment", @{thm Neigung_Moment})
5.23 + Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("Neigung_Moment", @{thm Neigung_Moment})
5.24 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
5.25 - make_thm @{theory} "IsacKnowledge" ("Querkraft_Belastung", @{thm Querkraft_Belastung})
5.26 + Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("Querkraft_Belastung", @{thm Querkraft_Belastung})
5.27 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
5.28 - make_thm @{theory} "IsacKnowledge" ("Querkraft_Moment", @{thm Querkraft_Moment})
5.29 + Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("Querkraft_Moment", @{thm Querkraft_Moment})
5.30 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
5.31 - make_thm @{theory} "IsacKnowledge" ("make_fun_explicit", @{thm make_fun_explicit})
5.32 + Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("make_fun_explicit", @{thm make_fun_explicit})
5.33 ["Walther Neuper 2005 supported by a grant from NMI Austria"]]
5.34 \<close>
5.35
6.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Wed Apr 21 11:47:33 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Apr 22 12:49:13 2021 +0200
6.3 @@ -53,7 +53,7 @@
6.4 subsubsection \<open>From rule-sets collect theorems, which have been taken from Isabelle\<close>
6.5 ML \<open>
6.6 val isacrlsthms = (*length = 460*)
6.7 - thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : ThmC.T list
6.8 + Thy_Hierarchy.thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : ThmC.T list
6.9
6.10 val rlsthmsNOTisac = isacrlsthms (*length = 36*)
6.11 |> filter (fn (deriv, _) =>
6.12 @@ -77,9 +77,9 @@
6.13 \<close>
6.14 ML \<open>
6.15 val thydata_list = (* SEE NOTE ABOVE *)
6.16 - collect_part "IsacKnowledge" knowledge_parent knowthys' @
6.17 - (map (collect_isab "Isabelle") rlsthmsNOTisac) @
6.18 - collect_part "IsacScripts" proglang_parent progthys'
6.19 + Thy_Hierarchy.collect_part "IsacKnowledge" knowledge_parent knowthys' @
6.20 + (map (Thy_Hierarchy.collect_isab "Isabelle") rlsthmsNOTisac) @
6.21 + Thy_Hierarchy.collect_part "IsacScripts" proglang_parent progthys'
6.22 : (Thy_Write.theID * Thy_Write.thydata) list
6.23 \<close>
6.24 ML \<open>
6.25 @@ -91,7 +91,7 @@
6.26 \<close> ML \<open>
6.27 "~~~~~ fun collect_part , args:"; val (part, parent, thys) = ("IsacKnowledge", knowledge_parent, knowthys');
6.28 \<close> ML \<open>
6.29 - val xxx = (flat (map (collect_thms part) thys))
6.30 + val xxx = (flat (map (Thy_Hierarchy.collect_thms part) thys))
6.31 \<close> ML \<open> (*isa*)
6.32 length thys = 32;
6.33 length xxx = 471
6.34 @@ -233,16 +233,8 @@
6.35 http://www.ist.tugraz.at/isac/Generate_representations_for_ISAC_Knowledge#Step_1:_Generate_XML_representation_from_SML
6.36
6.37 val path = "/tmp/xmldata/";
6.38 - thy_hierarchy2file (path ^ "thy/");
6.39 - thes2file (path ^ "thy/");
6.40 pbl_hierarchy2file (path ^ "pbl/");
6.41 - pbls2file (path ^ "pbl/");
6.42 met_hierarchy2file (path ^ "met/");
6.43 - mets2file (path ^ "met/");
6.44 -
6.45 - Adjust ''val path'' (for details see wiki) and copy line for line
6.46 - into an ML-block.
6.47 - Scroll down the Output window and look for potential error messages.
6.48 \<close>
6.49
6.50 section \<open>Link KEStore_Elems to completed IsacKnowledge\<close>