equal
deleted
inserted
replaced
102 "prepare ISAC Computer-Algebra System and register it to Knowledge Store" |
102 "prepare ISAC Computer-Algebra System and register it to Knowledge Store" |
103 (Parse.term -- (\<^keyword>\<open>=\<close> |-- |
103 (Parse.term -- (\<^keyword>\<open>=\<close> |-- |
104 Parse.!!! (Parse.ML_source -- parse_theory -- parse_problem -- parse_method)) |
104 Parse.!!! (Parse.ML_source -- parse_theory -- parse_problem -- parse_method)) |
105 >> (fn (term, (((source, thry), pbl), met)) => Toplevel.theory (fn thy => |
105 >> (fn (term, (((source, thry), pbl), met)) => Toplevel.theory (fn thy => |
106 let |
106 let |
107 val t = TermC.parse (Proof_Context.init_global thy) term; |
107 (*/------------ replace by ParseC.term_position ------------------\*) |
|
108 val SOME t = ParseC.term_opt (Proof_Context.init_global thy) term; |
|
109 (*\------------ replace by ParseC.term_position ------------------/*) |
108 val pblID = References_Def.explode_id pbl; |
110 val pblID = References_Def.explode_id pbl; |
109 val metID = References_Def.explode_id met; |
111 val metID = References_Def.explode_id met; |
110 val set_data = |
112 val set_data = |
111 ML_Context.expression (Input.pos_of source) |
113 ML_Context.expression (Input.pos_of source) |
112 (ml "Theory.setup (CAS_Def.set_data (" @ ML_Lex.read_source source @ ml "))") |
114 (ml "Theory.setup (CAS_Def.set_data (" @ ML_Lex.read_source source @ ml "))") |