author | wenzelm |
Fri, 18 Jan 2013 16:20:09 +0100 | |
changeset 50974 | 55f8bd61b029 |
parent 48897 | 873fdafc5b09 |
permissions | -rw-r--r-- |
21637 | 1 |
(* Title: Pure/ProofGeneral/pgip_isabelle.ML |
2 |
Author: David Aspinall |
|
3 |
||
22165 | 4 |
Prover-side PGIP abstraction: Isabelle configuration and mapping to Isabelle types. |
21637 | 5 |
*) |
6 |
||
7 |
signature PGIP_ISABELLE = |
|
8 |
sig |
|
9 |
val isabelle_pgml_version_supported : string |
|
10 |
val isabelle_pgip_version_supported : string |
|
23603 | 11 |
val systemid : string |
23799 | 12 |
val accepted_inputs : (string * bool * (string list)) list |
22165 | 13 |
|
14 |
val location_of_position : Position.T -> PgipTypes.location |
|
22403 | 15 |
|
16 |
(* Additional types of objects in Isar scripts *) |
|
17 |
||
18 |
val ObjTheoryBody : PgipTypes.objtype |
|
19 |
val ObjTheoryDecl : PgipTypes.objtype |
|
20 |
val ObjTheoryBodySubsection : PgipTypes.objtype |
|
21 |
val ObjProofBody : PgipTypes.objtype |
|
22 |
val ObjFormalComment : PgipTypes.objtype |
|
23 |
val ObjClass : PgipTypes.objtype |
|
24 |
val ObjTheoremSet : PgipTypes.objtype |
|
25 |
val ObjOracle : PgipTypes.objtype |
|
26 |
val ObjLocale : PgipTypes.objtype |
|
23799 | 27 |
|
21637 | 28 |
end |
29 |
||
30 |
structure PgipIsabelle : PGIP_ISABELLE = |
|
31 |
struct |
|
32 |
||
23603 | 33 |
val isabelle_pgml_version_supported = "2.0"; |
21637 | 34 |
val isabelle_pgip_version_supported = "2.0" |
23603 | 35 |
val systemid = "Isabelle" |
21637 | 36 |
|
23799 | 37 |
|
21637 | 38 |
(** Accepted commands **) |
39 |
||
40 |
local |
|
41 |
||
42 |
(* These element names are a subset of those in pgip_input.ML. |
|
43 |
They must be handled in proof_general_pgip.ML/process_pgip_element. *) |
|
23799 | 44 |
|
21637 | 45 |
val accepted_names = |
46 |
(* not implemented: "askconfig", "forget", "restoregoal" *) |
|
47 |
["askpgip","askpgml","askprefs","getpref","setpref", |
|
48 |
"proverinit","proverexit","startquiet","stopquiet", |
|
49 |
"pgmlsymbolson", "pgmlsymbolsoff", |
|
23799 | 50 |
"dostep", "undostep", "redostep", "abortgoal", |
21637 | 51 |
"askids", "showid", "askguise", |
52 |
"parsescript", |
|
53 |
"showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc", |
|
54 |
"doitem", "undoitem", "redoitem", "abortheory", |
|
55 |
"retracttheory", "loadfile", "openfile", "closefile", |
|
56 |
"abortfile", "retractfile", "changecwd", "systemcmd"]; |
|
57 |
||
23799 | 58 |
fun element_async p = |
59 |
false (* single threaded only *) |
|
21637 | 60 |
|
61 |
fun supported_optional_attrs p = (case p of |
|
23799 | 62 |
"undostep" => ["times"] |
63 |
(* TODO: we could probably extend these too: |
|
64 |
| "redostep" => ["times"] |
|
65 |
| "undoitem" => ["times"] |
|
66 |
| "redoitem" => ["times"] *) |
|
67 |
| _ => []) |
|
21637 | 68 |
in |
23799 | 69 |
val accepted_inputs = |
21637 | 70 |
(map (fn p=> (p, element_async p, supported_optional_attrs p)) |
71 |
accepted_names); |
|
72 |
end |
|
73 |
||
22165 | 74 |
|
23799 | 75 |
fun location_of_position pos = |
22165 | 76 |
let val line = Position.line_of pos |
23799 | 77 |
val (url,descr) = |
78 |
(case Position.file_of pos of |
|
79 |
NONE => (NONE, NONE) |
|
80 |
| SOME fname => |
|
81 |
let val path = Path.explode fname in |
|
48897 | 82 |
if File.exists path |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37939
diff
changeset
|
83 |
then (SOME (PgipTypes.pgipurl_of_path path), NONE) |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37939
diff
changeset
|
84 |
else (NONE, SOME fname) |
23799 | 85 |
end); |
23680 | 86 |
in |
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
41886
diff
changeset
|
87 |
{ descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE } |
23680 | 88 |
end |
22403 | 89 |
|
90 |
||
91 |
val [ObjTheoryBody, |
|
92 |
ObjTheoryDecl, |
|
93 |
ObjTheoryBodySubsection, |
|
94 |
ObjProofBody, |
|
95 |
ObjFormalComment, |
|
96 |
ObjClass, |
|
97 |
ObjTheoremSet, |
|
98 |
ObjOracle, |
|
99 |
ObjLocale] = |
|
23799 | 100 |
map PgipTypes.ObjOther |
101 |
["theory body", |
|
102 |
"theory declaration", |
|
103 |
"theory subsection", |
|
104 |
"proof body", |
|
105 |
"formal comment", |
|
106 |
"class", |
|
107 |
"theorem set declaration", |
|
108 |
"oracle", |
|
109 |
"locale"]; |
|
22403 | 110 |
|
21637 | 111 |
end |