src/Pure/ProofGeneral/pgip_isabelle.ML
author wenzelm
Fri, 18 Jan 2013 16:20:09 +0100
changeset 50974 55f8bd61b029
parent 48897 873fdafc5b09
permissions -rw-r--r--
added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
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
    Author:     David Aspinall
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     3
22165
eaec72532dd7 Add location_of_position. Needs work elsewhere.
aspinall
parents: 21940
diff changeset
     4
Prover-side PGIP abstraction: Isabelle configuration and mapping to Isabelle types.
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     5
*)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     6
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     7
signature PGIP_ISABELLE =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     8
sig
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     9
    val isabelle_pgml_version_supported : string
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    10
    val isabelle_pgip_version_supported : string
23603
4a2e36475367 Update PGML version, add system name
aspinall
parents: 22403
diff changeset
    11
    val systemid : string
23799
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    12
    val accepted_inputs : (string * bool * (string list)) list
22165
eaec72532dd7 Add location_of_position. Needs work elsewhere.
aspinall
parents: 21940
diff changeset
    13
eaec72532dd7 Add location_of_position. Needs work elsewhere.
aspinall
parents: 21940
diff changeset
    14
    val location_of_position : Position.T -> PgipTypes.location
22403
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    15
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    16
    (* Additional types of objects in Isar scripts *)
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    17
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    18
    val ObjTheoryBody : PgipTypes.objtype
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    19
    val ObjTheoryDecl : PgipTypes.objtype
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    20
    val ObjTheoryBodySubsection : PgipTypes.objtype
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    21
    val ObjProofBody : PgipTypes.objtype
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    22
    val ObjFormalComment : PgipTypes.objtype
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    23
    val ObjClass : PgipTypes.objtype
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    24
    val ObjTheoremSet : PgipTypes.objtype
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    25
    val ObjOracle : PgipTypes.objtype
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    26
    val ObjLocale : PgipTypes.objtype
23799
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    27
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    28
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    29
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    30
structure PgipIsabelle : PGIP_ISABELLE =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    31
struct
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    32
23603
4a2e36475367 Update PGML version, add system name
aspinall
parents: 22403
diff changeset
    33
val isabelle_pgml_version_supported = "2.0";
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    34
val isabelle_pgip_version_supported = "2.0"
23603
4a2e36475367 Update PGML version, add system name
aspinall
parents: 22403
diff changeset
    35
val systemid = "Isabelle"
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    36
23799
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    37
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    38
(** Accepted commands **)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    39
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    40
local
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    41
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    42
    (* These element names are a subset of those in pgip_input.ML.
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    43
       They must be handled in proof_general_pgip.ML/process_pgip_element. *)
23799
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    44
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    45
    val accepted_names =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    46
    (* not implemented: "askconfig", "forget", "restoregoal" *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    47
    ["askpgip","askpgml","askprefs","getpref","setpref",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    48
     "proverinit","proverexit","startquiet","stopquiet",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    49
     "pgmlsymbolson", "pgmlsymbolsoff",
23799
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    50
     "dostep", "undostep", "redostep", "abortgoal",
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    51
     "askids", "showid", "askguise",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    52
     "parsescript",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    53
     "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    54
     "doitem", "undoitem", "redoitem", "abortheory",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    55
     "retracttheory", "loadfile", "openfile", "closefile",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    56
     "abortfile", "retractfile", "changecwd", "systemcmd"];
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    57
23799
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    58
    fun element_async p =
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    59
        false (* single threaded only *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    60
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    61
    fun supported_optional_attrs p = (case p of
23799
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    62
                                          "undostep" => ["times"]
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    63
                                        (* TODO: we could probably extend these too:
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    64
                                        | "redostep" => ["times"]
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    65
                                        | "undoitem" => ["times"]
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    66
                                        | "redoitem" => ["times"] *)
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    67
                                        | _ => [])
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    68
in
23799
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    69
val accepted_inputs =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    70
    (map (fn p=> (p, element_async p, supported_optional_attrs p))
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    71
         accepted_names);
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    72
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    73
22165
eaec72532dd7 Add location_of_position. Needs work elsewhere.
aspinall
parents: 21940
diff changeset
    74
23799
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    75
fun location_of_position pos =
22165
eaec72532dd7 Add location_of_position. Needs work elsewhere.
aspinall
parents: 21940
diff changeset
    76
    let val line = Position.line_of pos
23799
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    77
        val (url,descr) =
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    78
            (case Position.file_of pos of
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    79
               NONE => (NONE, NONE)
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    80
             | SOME fname =>
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    81
               let val path = Path.explode fname in
48897
873fdafc5b09 tuned signature;
wenzelm
parents: 43710
diff changeset
    82
                 if File.exists path
38133
987680d2e77d simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents: 37939
diff changeset
    83
                 then (SOME (PgipTypes.pgipurl_of_path path), NONE)
987680d2e77d simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents: 37939
diff changeset
    84
                 else (NONE, SOME fname)
23799
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
    85
               end);
23680
09ccdb1b93ba use Position.file_of;
wenzelm
parents: 23603
diff changeset
    86
    in
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 41886
diff changeset
    87
        { descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
23680
09ccdb1b93ba use Position.file_of;
wenzelm
parents: 23603
diff changeset
    88
    end
22403
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    89
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    90
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    91
val [ObjTheoryBody,
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    92
     ObjTheoryDecl,
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    93
     ObjTheoryBodySubsection,
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    94
     ObjProofBody,
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    95
     ObjFormalComment,
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    96
     ObjClass,
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    97
     ObjTheoremSet,
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    98
     ObjOracle,
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
    99
     ObjLocale] =
23799
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
   100
    map PgipTypes.ObjOther
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
   101
        ["theory body",
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
   102
         "theory declaration",
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
   103
         "theory subsection",
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
   104
         "proof body",
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
   105
         "formal comment",
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
   106
         "class",
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
   107
         "theorem set declaration",
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
   108
         "oracle",
20f58293fc5e tuned spacing;
wenzelm
parents: 23680
diff changeset
   109
         "locale"];
22403
12892a6677c6 Add Isabelle-specific objtypes
aspinall
parents: 22165
diff changeset
   110
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   111
end