equal
deleted
inserted
replaced
24 val parse_item: string parser -> 'a parser -> 'a parser |
24 val parse_item: string parser -> 'a parser -> 'a parser |
25 val parse_item_name: string parser -> string -> string parser |
25 val parse_item_name: string parser -> string -> string parser |
26 val parse_item_names: string parser -> string list parser |
26 val parse_item_names: string parser -> string list parser |
27 val parse_model_input: model_input parser |
27 val parse_model_input: model_input parser |
28 val parse_authors: string list parser |
28 val parse_authors: string list parser |
|
29 val parse_cas: Token.T list -> string option * Token.T list |
|
30 val parse_methods: string list parser |
|
31 val ml: string -> ML_Lex.token Antiquote.antiquote list |
29 |
32 |
30 val from_store: id -> T |
33 val from_store: id -> T |
31 end |
34 end |
32 |
35 |
33 (**) |
36 (**) |
156 parse_tagged_terms \<^keyword>\<open>Where\<close> "#Where" @@@ |
159 parse_tagged_terms \<^keyword>\<open>Where\<close> "#Where" @@@ |
157 parse_tagged_terms \<^keyword>\<open>Find\<close> "#Find" @@@ |
160 parse_tagged_terms \<^keyword>\<open>Find\<close> "#Find" @@@ |
158 parse_tagged_terms \<^keyword>\<open>Relate\<close> "#Relate"; |
161 parse_tagged_terms \<^keyword>\<open>Relate\<close> "#Relate"; |
159 |
162 |
160 val parse_authors = parse_item_names \<^keyword>\<open>Author\<close>; |
163 val parse_authors = parse_item_names \<^keyword>\<open>Author\<close>; |
|
164 val parse_cas = Scan.option (parse_item \<^keyword>\<open>CAS\<close> Parse.term); |
|
165 val parse_methods = parse_item_names \<^keyword>\<open>Method\<close>; |
|
166 val ml = ML_Lex.read; |
161 |
167 |
162 |
168 |
163 (* command definition *) |
169 (* command definition *) |
164 |
170 |
165 local |
171 local |
166 |
|
167 val parse_methods = parse_item_names \<^keyword>\<open>Method\<close>; |
|
168 val parse_cas = Scan.option (parse_item \<^keyword>\<open>CAS\<close> Parse.term); |
|
169 |
|
170 val ml = ML_Lex.read; |
|
171 |
172 |
172 val _ = |
173 val _ = |
173 Outer_Syntax.command \<^command_keyword>\<open>problem\<close> |
174 Outer_Syntax.command \<^command_keyword>\<open>problem\<close> |
174 "prepare ISAC problem type and register it to Knowledge Store" |
175 "prepare ISAC problem type and register it to Knowledge Store" |
175 (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name -- |
176 (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name -- |