src/Pure/ProofGeneral/pgip_isabelle.ML

ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;

(*  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


fun location_of_position pos =
    let val line = Position.line_of pos
        val column = Position.column_of pos
        val (url,descr) =
            (case Position.file_of pos of
               NONE => (NONE, NONE)
             | SOME fname =>
               let val path = Path.explode fname in
                 case ThyLoad.check_file Path.current path of
                   SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
                 | NONE => (NONE, SOME fname)
               end);
    in
        { descr=descr, url=url, line=line, column=column, 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