equal
deleted
inserted
replaced
|
1 (* Title: src/Tools/isac/BridgeJEdit/parseC.sml |
|
2 Author: Walther Neuper, JKU Linz |
|
3 (c) due to copyright terms |
|
4 |
|
5 Outer syntax for Isabelle/Isac. Compare src/Pure/Pure.thy |
|
6 *) |
|
7 |
|
8 theory Isac |
|
9 imports "~~/src/Tools/isac/MathEngine/MathEngine" |
|
10 keywords |
|
11 (* this has a type and thus is a "major keyword" *) |
|
12 "ISAC" :: diag |
|
13 (* the following are without type: "minor keywords" *) |
|
14 and "Problem" (* root-problem + recursively in Solution *) |
|
15 and "Specification" "Model" "References" "Solution" (* structure only *) |
|
16 and "Given" "Find" "Relate" "Where" (* await input of term *) |
|
17 and "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *) |
|
18 "RProblem" "RMethod" (* await input of string list *) |
|
19 and "Tactic" (* optionally repeated with each step 0..end of calculation *) |
|
20 begin |
|
21 ML_file parseC.sml |
|
22 |
|
23 ML \<open> |
|
24 \<close> ML \<open> |
|
25 ParseC.problem (* not yet used *) |
|
26 \<close> ML \<open> |
|
27 \<close> |
|
28 |
|
29 (** setup command_keyword ISAC **) |
|
30 ML \<open> |
|
31 \<close> ML \<open> |
|
32 val _ = |
|
33 Outer_Syntax.command @{command_keyword ISAC} "embedded ISAC language" |
|
34 (Parse.input ((**)Parse.cartouche (** )--(**) ParseC.problem( **)) >> (fn input => |
|
35 Toplevel.keep (fn _ => ignore (ML_Lex.read_source input)))) |
|
36 \<close> ML \<open> |
|
37 \<close> |
|
38 |
|
39 end |