(*  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 (url,descr) = 

	    (case Position.file_of pos of

	       NONE => (NONE, NONE)

	     | 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);

    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