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