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