equal
deleted
inserted
replaced
16 |
16 |
17 ML_file "parseC.sml" |
17 ML_file "parseC.sml" |
18 ML_file "preliminary.sml" |
18 ML_file "preliminary.sml" |
19 |
19 |
20 section \<open>new code for Outer_Syntax Example ...\<close> |
20 section \<open>new code for Outer_Syntax Example ...\<close> |
21 text \<open> UPDATE: |
21 text \<open> |
22 1. The code re-uses Makarius' \<open>Outer_Syntax.command..problem ..\<close> to a maximal extent. |
22 stepwise development to be inspected from |
23 2. GOON |
23 https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080 |
|
24 onwards. |
24 \<close> |
25 \<close> |
25 |
26 |
26 ML \<open> |
27 ML \<open> |
27 \<close> ML \<open> |
28 \<close> ML \<open> |
28 \<close> ML \<open> |
29 \<close> ML \<open> |
61 val arg = Problem.prep_input thy name maa Problem.id_empty (pblID, model_input, input, cas, metIDs); |
62 val arg = Problem.prep_input thy name maa Problem.id_empty (pblID, model_input, input, cas, metIDs); |
62 in KEStore_Elems.add_pbts [arg] thy end))) |
63 in KEStore_Elems.add_pbts [arg] thy end))) |
63 |
64 |
64 in end; |
65 in end; |
65 \<close> ML \<open> |
66 \<close> ML \<open> |
66 Input.pos_of: Input.source -> Position.T |
|
67 \<close> ML \<open> |
67 \<close> ML \<open> |
68 Position.none |
|
69 \<close> ML \<open> |
68 \<close> ML \<open> |
70 \<close> |
69 \<close> |
71 |
70 |
72 |
71 |
73 end |
72 end |