src/Tools/isac/BridgeJEdit/Calculation.thy
changeset 60447 15951e1ea391
parent 60446 7a228201097c
child 60450 832961f676c3
     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 ->