src/Pure/ProofGeneral/pgip_isabelle.ML
author wenzelm
Fri Jun 13 21:04:42 2008 +0200 (2008-06-13)
changeset 27195 bbf4cbc69243
parent 26005 431ab3907291
child 29606 fedb8be05f24
permissions -rw-r--r--
map_const: soft version, no failure here;
     1 (*  Title:      Pure/ProofGeneral/pgip_isabelle.ML
     2     ID:         $Id$
     3     Author:     David Aspinall
     4 
     5 Prover-side PGIP abstraction: Isabelle configuration and mapping to Isabelle types.
     6 *)
     7 
     8 signature PGIP_ISABELLE =
     9 sig
    10     val isabelle_pgml_version_supported : string
    11     val isabelle_pgip_version_supported : string
    12     val systemid : string
    13     val accepted_inputs : (string * bool * (string list)) list
    14 
    15     val location_of_position : Position.T -> PgipTypes.location
    16 
    17     (* Additional types of objects in Isar scripts *)
    18 
    19     val ObjTheoryBody : PgipTypes.objtype
    20     val ObjTheoryDecl : PgipTypes.objtype
    21     val ObjTheoryBodySubsection : PgipTypes.objtype
    22     val ObjProofBody : PgipTypes.objtype
    23     val ObjFormalComment : PgipTypes.objtype
    24     val ObjClass : PgipTypes.objtype
    25     val ObjTheoremSet : PgipTypes.objtype
    26     val ObjOracle : PgipTypes.objtype
    27     val ObjLocale : PgipTypes.objtype
    28 
    29 end
    30 
    31 structure PgipIsabelle : PGIP_ISABELLE =
    32 struct
    33 
    34 val isabelle_pgml_version_supported = "2.0";
    35 val isabelle_pgip_version_supported = "2.0"
    36 val systemid = "Isabelle"
    37 
    38 
    39 (** Accepted commands **)
    40 
    41 local
    42 
    43     (* These element names are a subset of those in pgip_input.ML.
    44        They must be handled in proof_general_pgip.ML/process_pgip_element. *)
    45 
    46     val accepted_names =
    47     (* not implemented: "askconfig", "forget", "restoregoal" *)
    48     ["askpgip","askpgml","askprefs","getpref","setpref",
    49      "proverinit","proverexit","startquiet","stopquiet",
    50      "pgmlsymbolson", "pgmlsymbolsoff",
    51      "dostep", "undostep", "redostep", "abortgoal",
    52      "askids", "showid", "askguise",
    53      "parsescript",
    54      "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
    55      "doitem", "undoitem", "redoitem", "abortheory",
    56      "retracttheory", "loadfile", "openfile", "closefile",
    57      "abortfile", "retractfile", "changecwd", "systemcmd"];
    58 
    59     fun element_async p =
    60         false (* single threaded only *)
    61 
    62     fun supported_optional_attrs p = (case p of
    63                                           "undostep" => ["times"]
    64                                         (* TODO: we could probably extend these too:
    65                                         | "redostep" => ["times"]
    66                                         | "undoitem" => ["times"]
    67                                         | "redoitem" => ["times"] *)
    68                                         | _ => [])
    69 in
    70 val accepted_inputs =
    71     (map (fn p=> (p, element_async p, supported_optional_attrs p))
    72          accepted_names);
    73 end
    74 
    75 
    76 fun location_of_position pos =
    77     let val line = Position.line_of pos
    78         val column = Position.column_of pos
    79         val (url,descr) =
    80             (case Position.file_of pos of
    81                NONE => (NONE, NONE)
    82              | SOME fname =>
    83                let val path = Path.explode fname in
    84                  case ThyLoad.check_file Path.current path of
    85                    SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
    86                  | NONE => (NONE, SOME fname)
    87                end);
    88     in
    89         { descr=descr, url=url, line=line, column=column, char=NONE, length=NONE }
    90     end
    91 
    92 
    93 val [ObjTheoryBody,
    94      ObjTheoryDecl,
    95      ObjTheoryBodySubsection,
    96      ObjProofBody,
    97      ObjFormalComment,
    98      ObjClass,
    99      ObjTheoremSet,
   100      ObjOracle,
   101      ObjLocale] =
   102     map PgipTypes.ObjOther
   103         ["theory body",
   104          "theory declaration",
   105          "theory subsection",
   106          "proof body",
   107          "formal comment",
   108          "class",
   109          "theorem set declaration",
   110          "oracle",
   111          "locale"];
   112 
   113 end