|
1 (* Title: Pure/ProofGeneral/pgip_isabelle.ML |
|
2 ID: $Id$ |
|
3 Author: David Aspinall |
|
4 |
|
5 Prover-side PGIP abstraction: Isabelle configuration |
|
6 *) |
|
7 |
|
8 signature PGIP_ISABELLE = |
|
9 sig |
|
10 val isabelle_pgml_version_supported : string |
|
11 val isabelle_pgip_version_supported : string |
|
12 val accepted_inputs : (string * bool * (string list)) list |
|
13 end |
|
14 |
|
15 structure PgipIsabelle : PGIP_ISABELLE = |
|
16 struct |
|
17 |
|
18 val isabelle_pgml_version_supported = "1.0"; |
|
19 val isabelle_pgip_version_supported = "2.0" |
|
20 |
|
21 (** Accepted commands **) |
|
22 |
|
23 local |
|
24 |
|
25 (* These element names are a subset of those in pgip_input.ML. |
|
26 They must be handled in proof_general_pgip.ML/process_pgip_element. *) |
|
27 |
|
28 val accepted_names = |
|
29 (* not implemented: "askconfig", "forget", "restoregoal" *) |
|
30 ["askpgip","askpgml","askprefs","getpref","setpref", |
|
31 "proverinit","proverexit","startquiet","stopquiet", |
|
32 "pgmlsymbolson", "pgmlsymbolsoff", |
|
33 "dostep", "undostep", "redostep", "abortgoal", |
|
34 "askids", "showid", "askguise", |
|
35 "parsescript", |
|
36 "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc", |
|
37 "doitem", "undoitem", "redoitem", "abortheory", |
|
38 "retracttheory", "loadfile", "openfile", "closefile", |
|
39 "abortfile", "retractfile", "changecwd", "systemcmd"]; |
|
40 |
|
41 fun element_async p = |
|
42 false (* single threaded only *) |
|
43 |
|
44 fun supported_optional_attrs p = (case p of |
|
45 "undostep" => ["times"] |
|
46 (* TODO: we could probably extend these too: |
|
47 | "redostep" => ["times"] |
|
48 | "undoitem" => ["times"] |
|
49 | "redoitem" => ["times"] *) |
|
50 | _ => []) |
|
51 in |
|
52 val accepted_inputs = |
|
53 (map (fn p=> (p, element_async p, supported_optional_attrs p)) |
|
54 accepted_names); |
|
55 end |
|
56 |
|
57 end |
|
58 |