1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Jun 01 12:27:05 2022 +0200
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Jun 01 13:36:28 2022 +0200
1.3 @@ -76,17 +76,22 @@
1.4 (Parse.name --
1.5 Parse.!!! ( \<^keyword>\<open>=\<close> |-- Problem.parse_authors --
1.6 Problem.parse_methods -- Problem.parse_cas -- Problem.parse_model_input)(*/* ))( *\*) >>
1.7 - (fn (_(*name*), (((_(*maa*), mets), _(*cas*)), model_input)) =>
1.8 + (fn (pblID, (((_(*maa*), mets), _(*cas*)), model_input)) =>
1.9 Toplevel.theory (fn thy =>
1.10 let
1.11 + val pblID = References_Def.explode_id pblID;
1.12 val metIDs = map References_Def.explode_id mets;
1.13 - val input = update_state (model_input, (ThyC.id_empty, ["Biegelinien"], hd metIDs))
1.14 + val input = update_state (model_input, (ThyC.id_empty, pblID, hd metIDs))
1.15 Ctree.EmptyPtree;
1.16 in set_data input thy end)));
1.17 \<close> ML \<open>
1.18 +\<close> ML \<open>
1.19 +References_Def.explode_id: string -> References_Def.id
1.20 +\<close> ML \<open>
1.21 +\<close> ML \<open>
1.22 (*/----------------------------------------------------------------------------\*)
1.23 Parse.name --
1.24 - Parse.!!! ( \<^keyword>\<open>=\<close> |-- Problem.parse_authors --
1.25 + Parse.!!! ((**) \<^keyword>\<open>=\<close> |-- Problem.parse_authors --
1.26 Problem.parse_methods -- Problem.parse_cas -- Problem.parse_model_input)
1.27 (*\----------------------------------------------------------------------------/*)
1.28 : Token.T list ->