(* Title: Pure/ProofGeneral/pgip_isabelle.ML
ID: $Id$
Author: David Aspinall
Prover-side PGIP abstraction: Isabelle configuration and mapping to Isabelle types.
*)
signature PGIP_ISABELLE =
sig
val isabelle_pgml_version_supported : string
val isabelle_pgip_version_supported : string
val systemid : string
val accepted_inputs : (string * bool * (string list)) list
val location_of_position : Position.T -> PgipTypes.location
(* Additional types of objects in Isar scripts *)
val ObjTheoryBody : PgipTypes.objtype
val ObjTheoryDecl : PgipTypes.objtype
val ObjTheoryBodySubsection : PgipTypes.objtype
val ObjProofBody : PgipTypes.objtype
val ObjFormalComment : PgipTypes.objtype
val ObjClass : PgipTypes.objtype
val ObjTheoremSet : PgipTypes.objtype
val ObjOracle : PgipTypes.objtype
val ObjLocale : PgipTypes.objtype
end
structure PgipIsabelle : PGIP_ISABELLE =
struct
val isabelle_pgml_version_supported = "2.0";
val isabelle_pgip_version_supported = "2.0"
val systemid = "Isabelle"
(** Accepted commands **)
local
(* These element names are a subset of those in pgip_input.ML.
They must be handled in proof_general_pgip.ML/process_pgip_element. *)
val accepted_names =
(* not implemented: "askconfig", "forget", "restoregoal" *)
["askpgip","askpgml","askprefs","getpref","setpref",
"proverinit","proverexit","startquiet","stopquiet",
"pgmlsymbolson", "pgmlsymbolsoff",
"dostep", "undostep", "redostep", "abortgoal",
"askids", "showid", "askguise",
"parsescript",
"showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
"doitem", "undoitem", "redoitem", "abortheory",
"retracttheory", "loadfile", "openfile", "closefile",
"abortfile", "retractfile", "changecwd", "systemcmd"];
fun element_async p =
false (* single threaded only *)
fun supported_optional_attrs p = (case p of
"undostep" => ["times"]
(* TODO: we could probably extend these too:
| "redostep" => ["times"]
| "undoitem" => ["times"]
| "redoitem" => ["times"] *)
| _ => [])
in
val accepted_inputs =
(map (fn p=> (p, element_async p, supported_optional_attrs p))
accepted_names);
end
(* Now we have to parse strings constructed elsewhere in Isabelle, which is silly!
This is another case where Isabelle should use structured types
from the ground up to help its interfaces, instead of just plain
strings.
*)
fun unquote s = case explode s of
"\""::xs => (case (rev xs) of
"\""::_ => SOME (String.substring(s,1,(String.size s) - 2))
| _ => NONE)
| _ => NONE
fun location_of_position pos =
let val line = Position.line_of pos
val (url,descr) =
(case Position.name_of pos of
NONE => (NONE,NONE)
| SOME possiblyfile =>
(case unquote possiblyfile of
SOME fname => let val path = (Path.explode fname) in
case ThyLoad.check_file NONE path of
SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
| NONE => (NONE,SOME fname)
end
| _ => (NONE,SOME possiblyfile)))
in
{ descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
end
val [ObjTheoryBody,
ObjTheoryDecl,
ObjTheoryBodySubsection,
ObjProofBody,
ObjFormalComment,
ObjClass,
ObjTheoremSet,
ObjOracle,
ObjLocale] =
map PgipTypes.ObjOther
["theory body",
"theory declaration",
"theory subsection",
"proof body",
"formal comment",
"class",
"theorem set declaration",
"oracle",
"locale"];
end