src/Pure/ProofGeneral/proof_general_pgip.ML
author wenzelm
Thu, 15 Apr 2010 15:38:58 +0200
changeset 36148 4ddcc2b07891
parent 33389 bb3a5fa94a91
child 36689 379f5b1e7f91
permissions -rw-r--r--
spelling;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     1
(*  Title:      Pure/ProofGeneral/proof_general_pgip.ML
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     2
    Author:     David Aspinall and Markus Wenzel
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     3
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     4
Isabelle configuration for Proof General using PGIP protocol.
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
     5
See http://proofgeneral.inf.ed.ac.uk/kit
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 PROOF_GENERAL_PGIP =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     9
sig
28100
7650d5e0f8fb refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents: 28097
diff changeset
    10
  val new_thms_deps: theory -> theory -> string list * string list
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
    11
  val init_pgip: bool -> unit             (* main PGIP loop with true; fail with false *)
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents: 21637
diff changeset
    12
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
    13
  (* These two are just to support the semi-PGIP Emacs mode *)
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
    14
  val init_pgip_channel: (string -> unit) -> unit
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
    15
  val process_pgip: string -> unit
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
    16
23435
061f28854017 Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents: 23226
diff changeset
    17
  (* More message functions... *)
061f28854017 Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents: 23226
diff changeset
    18
  val nonfatal_error : string -> unit     (* recoverable (batch) error: carry on scripting *)
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
    19
  val log_msg : string -> unit            (* for internal log messages *)
23759
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
    20
  val error_with_pos : PgipTypes.displayarea -> PgipTypes.fatality -> Position.T -> string -> unit
22159
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
    21
22163
a586b0af857e Expose currently open file
aspinall
parents: 22159
diff changeset
    22
  val get_currently_open_file : unit -> Path.T option  (* interface focus *)
28588
cdf21c1dfb19 CRITICAL access to preferences;
wenzelm
parents: 28504
diff changeset
    23
  val add_preference: string -> Preferences.preference -> unit
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    24
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    25
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    26
structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    27
struct
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    28
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    29
open Pgip;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    30
21949
046e0482f0a1 removed obsolete context_thy etc.;
wenzelm
parents: 21940
diff changeset
    31
23641
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
    32
(** print mode **)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    33
22408
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
    34
val proof_generalN = "ProofGeneral";
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
    35
val pgmlsymbols_flag = Unsynchronized.ref true;
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    36
23641
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
    37
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
    38
(* assembling and issuing PGIP packets *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    39
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
    40
val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
    41
val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref;
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    42
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    43
local
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    44
  val pgip_class  = "pg"
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    45
  val pgip_tag = "Isabelle/Isar"
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
    46
  val pgip_id = Unsynchronized.ref ""
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
    47
  val pgip_seq = Unsynchronized.ref 0
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
    48
  fun pgip_serial () = Unsynchronized.inc pgip_seq
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    49
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    50
  fun assemble_pgips pgips =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
    51
    Pgip { tag = SOME pgip_tag,
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
    52
           class = pgip_class,
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    53
           seq = pgip_serial (),
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    54
           id = ! pgip_id,
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    55
           destid = ! pgip_refid,
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
    56
           (* destid=refid since Isabelle only communicates back to sender *)
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    57
           refid = ! pgip_refid,
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    58
           refseq = ! pgip_refseq,
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
    59
           content = pgips }
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    60
in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    61
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    62
fun init_pgip_session_id () =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    63
    pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    64
               getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    65
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    66
fun matching_pgip_id id = (id = ! pgip_id)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    67
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
    68
val output_xml_fn = Unsynchronized.ref Output.writeln_default
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    69
fun output_xml s = ! output_xml_fn (XML.string_of s);
23641
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
    70
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    71
val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
23759
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
    72
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    73
val output_pgmlterm = XML.string_of o Pgml.pgmlterm_to_xml;
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    74
val output_pgmltext = XML.string_of o Pgml.pgml_to_xml;
23759
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
    75
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
    76
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
    77
fun issue_pgip_rawtext str =
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    78
  output_xml (PgipOutput.output (assemble_pgips (YXML.parse_body str)));
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    79
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    80
fun issue_pgip pgipop =
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    81
  output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop]));
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    82
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    83
end;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    84
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    85
23641
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
    86
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    87
(** messages and notification **)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    88
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    89
(* PGML terms *)
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    90
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    91
local
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    92
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    93
fun pgml_sym s =
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    94
  if ! pgmlsymbols_flag then
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    95
    (case Symbol.decode s of
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    96
      Symbol.Sym name => Pgml.Sym {name = name, content = s}
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    97
    | _ => Pgml.Str s)
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
    98
  else Pgml.Str s;
23759
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
    99
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   100
val pgml_syms = map pgml_sym o Symbol.explode;
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   101
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   102
val token_markups =
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   103
 [Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   104
  Markup.boundN, Markup.varN, Markup.skolemN];
23759
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
   105
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   106
in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   107
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   108
fun pgml_terms (XML.Elem (name, atts, body)) =
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   109
      if member (op =) token_markups name then
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   110
        let val content = pgml_syms (Buffer.content (fold XML.add_content body Buffer.empty))
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   111
        in [Pgml.Atoms {kind = SOME name, content = content}] end
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   112
      else
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   113
        let val content = maps pgml_terms body in
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   114
          if name = Markup.blockN then
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   115
            [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}]
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   116
          else if name = Markup.breakN then
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   117
            [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}]
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   118
          else if name = Markup.fbreakN then
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   119
            [Pgml.Break {mandatory = SOME true, indent = NONE}]
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   120
          else content
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   121
        end
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   122
  | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   123
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   124
end;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   125
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   126
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   127
(* messages *)
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   128
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   129
fun pgml area content =
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   130
  Pgml.Pgml {version = NONE, systemid = NONE, area = SOME area, content = content};
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   131
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   132
fun message_content default_area s =
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   133
  let
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   134
    val body = YXML.parse_body s;
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   135
    val area =
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   136
      (case body of
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   137
        [XML.Elem (name, _, _)] =>
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   138
          if name = Markup.stateN then PgipTypes.Display else default_area
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   139
      | _ => default_area);
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   140
  in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   141
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   142
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   143
fun normalmsg area s = issue_pgip
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   144
  (Normalresponse {content = [message_content area s]});
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   145
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   146
fun errormsg area fatality s = issue_pgip
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   147
  (Errorresponse {fatality = fatality, location = NONE, content = [message_content area s]});
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   148
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   149
(*error responses with useful locations*)
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   150
fun error_with_pos area fatality pos s = issue_pgip
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   151
  (Errorresponse {
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   152
    fatality = fatality,
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   153
    location = SOME (PgipIsabelle.location_of_position pos),
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   154
    content = [message_content area s]});
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   155
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   156
fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1);
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   157
fun nonfatal_error s = errormsg Message Nonfatal s;
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   158
fun log_msg s = errormsg Message Log s;
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   159
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   160
(* NB: all of standard functions print strings terminated with new lines, but we don't
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   161
   add new lines explicitly in PGIP: they are left implicit.  It means that PGIP messages
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   162
   can't be written without newlines. *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   163
fun setup_messages () =
23759
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
   164
 (Output.writeln_fn := (fn s => normalmsg Message s);
27604
6c347b96d941 added status channel;
wenzelm
parents: 27578
diff changeset
   165
  Output.status_fn := (fn _ => ());
23840
0295493ba748 Direct priority and tracing channels properly.
aspinall
parents: 23834
diff changeset
   166
  Output.priority_fn := (fn s => normalmsg Status s);
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   167
  Output.tracing_fn := (fn s => normalmsg Tracing s);
23759
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
   168
  Output.warning_fn := (fn s => errormsg Message Warning s);
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
   169
  Output.error_fn := (fn s => errormsg Message Fatal s);
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
   170
  Output.debug_fn := (fn s => errormsg Message Debug s));
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   171
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   172
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   173
(* immediate messages *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   174
26706
4ea64590d28b replaced token translations by common markup;
wenzelm
parents: 26622
diff changeset
   175
fun tell_clear_goals () =
23759
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
   176
    issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Display [])] })
26706
4ea64590d28b replaced token translations by common markup;
wenzelm
parents: 26622
diff changeset
   177
fun tell_clear_response () =
23759
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
   178
    issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Message [])] })
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   179
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   180
fun tell_file_loaded completed path   =
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   181
    issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path,
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   182
                                  completed=completed})
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   183
fun tell_file_outdated completed path   =
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   184
    issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path,
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   185
                                    completed=completed})
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   186
fun tell_file_retracted completed path =
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   187
    issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path,
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   188
                                     completed=completed})
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   189
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   190
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   191
(* theory loader actions *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   192
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   193
local
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   194
  (* da: TODO: PGIP has a completed flag so the prover can indicate to the
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   195
     interface which files are busy performing a particular action.
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   196
     To make use of this we need to adjust the hook in thy_info.ML
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   197
     (may actually be difficult to tell the interface *which* action is in
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   198
      progress, but we could add a generic "Lock" action which uses
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   199
      informfileloaded: the broker/UI should not infer too much from incomplete
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   200
      operations).
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   201
   *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   202
fun trace_action action name =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   203
  if action = ThyInfo.Update then
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   204
    List.app (tell_file_loaded true) (ThyInfo.loaded_files name)
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   205
  else if action = ThyInfo.Outdate then
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   206
    List.app (tell_file_outdated true) (ThyInfo.loaded_files name)
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   207
  else if action = ThyInfo.Remove then
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   208
      List.app (tell_file_retracted true) (ThyInfo.loaded_files name)
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   209
  else ()
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   210
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   211
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   212
in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   213
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
26613
725a3d9011d1 ThyInfo.get_names;
wenzelm
parents: 26603
diff changeset
   214
  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   215
end;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   216
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   217
21949
046e0482f0a1 removed obsolete context_thy etc.;
wenzelm
parents: 21940
diff changeset
   218
(* get informed about files *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   219
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   220
val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   221
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   222
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   223
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   224
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   225
fun proper_inform_file_processed path state =
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   226
  let val name = thy_name path in
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   227
    if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   228
     (ThyInfo.touch_child_thys name;
24079
3ba5d68e076b ThyInfo.register_thy;
wenzelm
parents: 24067
diff changeset
   229
      ThyInfo.register_thy name handle ERROR msg =>
23913
fcfacb6670ed inform_file_processed: tuned msg, no state;
wenzelm
parents: 23884
diff changeset
   230
       (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   231
        tell_file_retracted true (Path.base path)))
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   232
    else raise Toplevel.UNDEF
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   233
  end;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   234
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   235
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   236
(* restart top-level loop (keeps most state information) *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   237
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   238
val welcome = priority o Session.welcome;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   239
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   240
fun restart () =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   241
    (sync_thy_loader ();
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   242
     tell_clear_goals ();
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   243
     tell_clear_response ();
29349
b49d8501720a Isar.init;
wenzelm
parents: 28817
diff changeset
   244
     Isar.init ();
27578
75945c883672 removed obsolete Toplevel.RESTART;
wenzelm
parents: 27565
diff changeset
   245
     welcome ());
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   246
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   247
28097
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   248
(* theorem dependencies *)
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   249
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   250
local
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   251
28809
7c2e1bbf3c36 retrieve thm deps from proof_body;
wenzelm
parents: 28588
diff changeset
   252
fun add_proof_body (PBody {thms, ...}) =
28817
c8cc94a470d4 proof_body/pthm: removed redundant types field;
wenzelm
parents: 28814
diff changeset
   253
  thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
28809
7c2e1bbf3c36 retrieve thm deps from proof_body;
wenzelm
parents: 28588
diff changeset
   254
7c2e1bbf3c36 retrieve thm deps from proof_body;
wenzelm
parents: 28588
diff changeset
   255
fun add_thm th =
28814
463c9e9111ae clarified Thm.proof_body_of vs. Thm.proof_of;
wenzelm
parents: 28809
diff changeset
   256
  (case Thm.proof_body_of th of 
28809
7c2e1bbf3c36 retrieve thm deps from proof_body;
wenzelm
parents: 28588
diff changeset
   257
    PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
7c2e1bbf3c36 retrieve thm deps from proof_body;
wenzelm
parents: 28588
diff changeset
   258
      if Thm.has_name_hint th andalso Thm.get_name_hint th = name
29635
31d14e9fa0da proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents: 29606
diff changeset
   259
      then add_proof_body (Future.join body)
28097
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   260
      else I
28809
7c2e1bbf3c36 retrieve thm deps from proof_body;
wenzelm
parents: 28588
diff changeset
   261
  | body => add_proof_body body);
7c2e1bbf3c36 retrieve thm deps from proof_body;
wenzelm
parents: 28588
diff changeset
   262
7c2e1bbf3c36 retrieve thm deps from proof_body;
wenzelm
parents: 28588
diff changeset
   263
in
28097
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   264
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   265
fun thms_deps ths =
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   266
  let
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   267
    (* FIXME proper derivation names!? *)
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   268
    val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
28809
7c2e1bbf3c36 retrieve thm deps from proof_body;
wenzelm
parents: 28588
diff changeset
   269
    val deps = Symtab.keys (fold add_thm ths Symtab.empty);
28097
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   270
  in (names, deps) end;
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   271
28100
7650d5e0f8fb refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents: 28097
diff changeset
   272
fun new_thms_deps thy thy' =
28097
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   273
  let
28100
7650d5e0f8fb refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents: 28097
diff changeset
   274
    val prev_facts = PureThy.facts_of thy;
7650d5e0f8fb refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents: 28097
diff changeset
   275
    val facts = PureThy.facts_of thy';
7650d5e0f8fb refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents: 28097
diff changeset
   276
  in thms_deps (maps #2 (Facts.dest_static [prev_facts] facts)) end;
28097
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   277
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   278
end;
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   279
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   280
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   281
(* theorem dependeny output *)
22408
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
   282
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
   283
val show_theorem_dependencies = Unsynchronized.ref false;
22408
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
   284
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   285
local
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   286
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   287
val spaces_quote = space_implode " " o map quote;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   288
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   289
fun thm_deps_message (thms, deps) =
28097
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   290
  let
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   291
    val valuethms = XML.Elem ("value", [("name", "thms")], [XML.Text thms]);
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   292
    val valuedeps = XML.Elem ("value", [("name", "deps")], [XML.Text deps]);
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   293
  in
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   294
    issue_pgip (Metainforesponse
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   295
      {attrs = [("infotype", "isabelle_theorem_dependencies")],
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   296
       content = [valuethms, valuedeps]})
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   297
  end;
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   298
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   299
in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   300
28103
b79e61861f0f simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents: 28100
diff changeset
   301
fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
28100
7650d5e0f8fb refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents: 28097
diff changeset
   302
  if ! show_theorem_dependencies andalso
28103
b79e61861f0f simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents: 28100
diff changeset
   303
    can Toplevel.theory_of state andalso Toplevel.is_theory state'
28100
7650d5e0f8fb refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents: 28097
diff changeset
   304
  then
7650d5e0f8fb refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents: 28097
diff changeset
   305
    let val (names, deps) = new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state') in
28097
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   306
      if null names orelse null deps then ()
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   307
      else thm_deps_message (spaces_quote names, spaces_quote deps)
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   308
    end
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   309
  else ());
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   310
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   311
end;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   312
28097
003dff7410c1 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents: 28066
diff changeset
   313
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   314
(** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   315
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   316
fun lexicalstructure_keywords () =
27353
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 27177
diff changeset
   317
    let val keywords = OuterKeyword.dest_keywords ()
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 27177
diff changeset
   318
        val commands = OuterKeyword.dest_commands ()
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 27177
diff changeset
   319
        fun keyword_elt kind keyword =
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 27177
diff changeset
   320
            XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   321
        in
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   322
            (* Also, note we don't call init_outer_syntax here to add interface commands,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   323
            but they should never appear in scripts anyway so it shouldn't matter *)
27353
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 27177
diff changeset
   324
            Lexicalstructure
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 27177
diff changeset
   325
              {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands}
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   326
        end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   327
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   328
(* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   329
   hooks needed in outer_syntax.ML to do that. *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   330
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   331
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   332
(* Configuration: GUI config, proverinfo messages *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   333
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   334
local
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   335
    val isabellewww = "http://isabelle.in.tum.de/"
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   336
    val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml"
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   337
    fun orenv v d = case getenv v of "" => d  | s => s
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   338
    fun config_file()  = orenv "ISABELLE_PGIPCONFIG" staticconfig
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   339
    fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   340
in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   341
fun send_pgip_config () =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   342
    let
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21655
diff changeset
   343
        val path = Path.explode (config_file())
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   344
        val ex = File.exists path
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   345
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   346
        val wwwpage =
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   347
            (Url.explode (isabelle_www()))
21969
a8bf1106cb7c removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   348
            handle ERROR _ =>
22699
938c1011ac94 removed unused Output.panic hook -- internal to PG wrapper;
wenzelm
parents: 22678
diff changeset
   349
                   (panic ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   350
                        Url.explode isabellewww)
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   351
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   352
        val proverinfo =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   353
            Proverinfo { name = "Isabelle",
26109
c69c3559355b more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents: 25847
diff changeset
   354
                         version = Distribution.version,
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   355
                         instance = Session.name(),
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   356
                         descr = "The Isabelle/Isar theorem prover",
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   357
                         url = wwwpage,
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   358
                         filenameextns = ".thy;" }
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   359
    in
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   360
        if ex then
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   361
            (issue_pgip proverinfo;
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   362
             issue_pgip_rawtext (File.read path);
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   363
             issue_pgip (lexicalstructure_keywords()))
22699
938c1011ac94 removed unused Output.panic hook -- internal to PG wrapper;
wenzelm
parents: 22678
diff changeset
   364
        else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   365
    end;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   366
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   367
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   368
22216
c3f5aa951a68 Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents: 22171
diff changeset
   369
(* Preferences: tweak for PGIP interfaces *)
c3f5aa951a68 Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents: 22171
diff changeset
   370
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
   371
val preferences = Unsynchronized.ref Preferences.pure_preferences;
22216
c3f5aa951a68 Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents: 22171
diff changeset
   372
28066
611e504c1191 extended interface to preferences to allow adding new ones
nipkow
parents: 28037
diff changeset
   373
fun add_preference cat pref =
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
   374
  CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref));
28066
611e504c1191 extended interface to preferences to allow adding new ones
nipkow
parents: 28037
diff changeset
   375
28588
cdf21c1dfb19 CRITICAL access to preferences;
wenzelm
parents: 28504
diff changeset
   376
fun setup_preferences_tweak () =
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
   377
  CRITICAL (fn () => Unsynchronized.change preferences
28588
cdf21c1dfb19 CRITICAL access to preferences;
wenzelm
parents: 28504
diff changeset
   378
   (Preferences.set_default ("show-question-marks", "false") #>
cdf21c1dfb19 CRITICAL access to preferences;
wenzelm
parents: 28504
diff changeset
   379
    Preferences.remove "show-question-marks" #>   (* we use markup, not ?s *)
cdf21c1dfb19 CRITICAL access to preferences;
wenzelm
parents: 28504
diff changeset
   380
    Preferences.remove "theorem-dependencies" #>  (* set internally *)
cdf21c1dfb19 CRITICAL access to preferences;
wenzelm
parents: 28504
diff changeset
   381
    Preferences.remove "full-proofs"));           (* set internally *)
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   382
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   383
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   384
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   385
(* Sending commands to Isar *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   386
26622
e8e81ddb8919 simplified isarcmd;
wenzelm
parents: 26613
diff changeset
   387
fun isarcmd s = Isar.>>> (OuterSyntax.parse Position.none s);
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   388
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   389
(* TODO:
27565
4bb03d4509e2 command 'redo' no longer available;
wenzelm
parents: 27353
diff changeset
   390
    - apply a command given a transition function;
21885
5a11263bd8cf Remove obsolete prefixes from error and warning messages.
aspinall
parents: 21867
diff changeset
   391
    - fix position from path of currently open file [line numbers risk garbling though].
5a11263bd8cf Remove obsolete prefixes from error and warning messages.
aspinall
parents: 21867
diff changeset
   392
*)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   393
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   394
(* load an arbitrary file (must be .thy or .ML) *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   395
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   396
fun use_thy_or_ml_file file =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   397
    let
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21655
diff changeset
   398
        val (path,extn) = Path.split_ext (Path.explode file)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   399
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   400
        case extn of
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   401
            "" => isarcmd ("use_thy " ^ quote (Path.implode path))
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   402
          | "thy" => isarcmd ("use_thy " ^ quote (Path.implode path))
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   403
          | "ML" => isarcmd ("use " ^ quote file)
22028
c13f6b5bf2b8 Be more chatty in PGIP file operations.
aspinall
parents: 22014
diff changeset
   404
          | other => error ("Don't know how to read a file with extension " ^ quote other)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   405
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   406
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   407
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   408
(******* PGIP actions *******)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   409
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   410
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   411
(* Responses to each of the PGIP input commands.
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   412
   These are programmed uniformly for extensibility. *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   413
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   414
fun askpgip (Askpgip _) =
23435
061f28854017 Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents: 23226
diff changeset
   415
    (issue_pgip
061f28854017 Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents: 23226
diff changeset
   416
         (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
061f28854017 Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents: 23226
diff changeset
   417
                     pgipelems = PgipIsabelle.accepted_inputs });
061f28854017 Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents: 23226
diff changeset
   418
     send_pgip_config())
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   419
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   420
fun askpgml (Askpgml _) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   421
    issue_pgip
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   422
        (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   423
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   424
fun askprefs (Askprefs _) =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   425
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   426
        fun preference_of {name, descr, default, pgiptype, get, set } =
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   427
            { name = name, descr = SOME descr, default = SOME default,
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   428
              pgiptype = pgiptype }
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   429
    in
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   430
        List.app (fn (prefcat, prefs) =>
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   431
                     issue_pgip (Hasprefs {prefcategory=SOME prefcat,
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   432
                                           prefs=map preference_of prefs}))
22216
c3f5aa951a68 Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents: 22171
diff changeset
   433
                 (!preferences)
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   434
    end
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   435
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   436
fun askconfig (Askconfig _) = () (* TODO: add config response *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   437
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   438
local
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   439
    fun lookuppref pref =
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   440
        case AList.lookup (op =)
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   441
                          (map (fn p => (#name p,p))
22216
c3f5aa951a68 Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents: 22171
diff changeset
   442
                               (maps snd (!preferences))) pref of
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   443
            NONE => error ("Unknown prover preference: " ^ quote pref)
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   444
          | SOME p => p
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   445
in
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   446
fun setpref (Setpref vs) =
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   447
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   448
        val name = #name vs
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   449
        val value = #value vs
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   450
        val set = #set (lookuppref name)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   451
    in
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   452
        set value
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   453
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   454
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   455
fun getpref (Getpref vs) =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   456
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   457
        val name = #name vs
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   458
        val get = #get (lookuppref name)
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   459
    in
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   460
        issue_pgip (Prefval {name=name, value=get ()})
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   461
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   462
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   463
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   464
fun proverinit _ = restart ()
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   465
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   466
fun proverexit _ = isarcmd "quit"
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   467
26706
4ea64590d28b replaced token translations by common markup;
wenzelm
parents: 26622
diff changeset
   468
fun set_proverflag_quiet b =
22408
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
   469
    isarcmd (if b then "disable_pr" else "enable_pr")
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   470
22408
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
   471
fun set_proverflag_pgmlsymbols b =
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
   472
    (pgmlsymbols_flag := b;
24614
a4b2eb0dd673 change print_mode: CRITICAL;
wenzelm
parents: 24244
diff changeset
   473
      NAMED_CRITICAL "print_mode" (fn () =>
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
   474
        Unsynchronized.change print_mode
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22408
diff changeset
   475
            (fn mode =>
24614
a4b2eb0dd673 change print_mode: CRITICAL;
wenzelm
parents: 24244
diff changeset
   476
                remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
22408
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
   477
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
   478
fun set_proverflag_thmdeps b =
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
   479
    (show_theorem_dependencies := b;
25223
7463251e7273 qualified Proofterm.proofs;
wenzelm
parents: 24867
diff changeset
   480
     Proofterm.proofs := (if b then 1 else 2))
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   481
22408
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
   482
fun setproverflag (Setproverflag vs) =
26706
4ea64590d28b replaced token translations by common markup;
wenzelm
parents: 26622
diff changeset
   483
    let
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22408
diff changeset
   484
        val flagname = #flagname vs
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22408
diff changeset
   485
        val value = #value vs
22408
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
   486
    in
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22408
diff changeset
   487
        (case flagname of
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22408
diff changeset
   488
             "quiet"            => set_proverflag_quiet value
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22408
diff changeset
   489
           | "pgmlsymbols"      => set_proverflag_pgmlsymbols value
26706
4ea64590d28b replaced token translations by common markup;
wenzelm
parents: 26622
diff changeset
   490
           | "metainfo:thmdeps" => set_proverflag_thmdeps value
4ea64590d28b replaced token translations by common markup;
wenzelm
parents: 26622
diff changeset
   491
           | _ => log_msg ("Unrecognised prover control flag: " ^
23801
20c0dd4f783f simplified using Markup.get_int;
wenzelm
parents: 23759
diff changeset
   492
                           (quote flagname) ^ " ignored."))
26706
4ea64590d28b replaced token translations by common markup;
wenzelm
parents: 26622
diff changeset
   493
    end
22408
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
   494
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   495
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   496
fun dostep (Dostep vs) =
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   497
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   498
        val text = #text vs
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   499
    in
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   500
        isarcmd text
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   501
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   502
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   503
fun undostep (Undostep vs) =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   504
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   505
        val times = #times vs
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   506
    in
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   507
        isarcmd ("undos_proof " ^ Int.toString times)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   508
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   509
27565
4bb03d4509e2 command 'redo' no longer available;
wenzelm
parents: 27353
diff changeset
   510
fun redostep _ = sys_error "redo unavailable"
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   511
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   512
fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   513
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   514
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   515
(*** PGIP identifier tables ***)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   516
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   517
(* TODO: these ones should be triggered by hooks after a
22159
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   518
   declaration addition/removal, to be sent automatically. *)
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   519
22159
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   520
fun addids t  = issue_pgip (Addids {idtables = [t]})
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   521
fun delids t  = issue_pgip (Delids {idtables = [t]})
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   522
27177
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   523
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   524
local
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   525
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   526
fun theory_facts name =
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   527
  let val thy = ThyInfo.get_theory name
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   528
  in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end;
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   529
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   530
fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   531
fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static);
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   532
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   533
in
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   534
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   535
fun askids (Askids vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   536
    let
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   537
        val url = #url vs            (* ask for identifiers within a file *)
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   538
        val thyname = #thyname vs    (* ask for identifiers within a theory *)
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   539
        val objtype = #objtype vs    (* ask for identifiers of a particular type *)
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   540
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   541
        fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   542
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   543
        fun setids t = issue_pgip (Setids {idtables = [t]})
22159
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   544
22225
30ab97554602 Fix tell_thm_deps to match changse in PureThy.
aspinall
parents: 22216
diff changeset
   545
        (* fake one-level nested "subtheories" by picking apart names. *)
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 29635
diff changeset
   546
        val immed_thms_of_thy = filter_out Long_Name.is_qualified o thms_of_thy
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 29635
diff changeset
   547
        fun thy_prefix s = case Long_Name.explode s of
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   548
                                    x::_::_ => SOME x  (* String.find? *)
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   549
                                  | _ => NONE
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   550
        fun subthys_of_thy s =
23178
07ba6b58b3d2 simplified/unified list fold;
wenzelm
parents: 22699
diff changeset
   551
            List.foldl  (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   552
                   (map thy_prefix (thms_of_thy s))
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   553
        fun subthms_of_thy thy =
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   554
            (case thy_prefix thy of
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   555
                 NONE => immed_thms_of_thy thy
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 29635
diff changeset
   556
               | SOME prf => filter (String.isPrefix (unprefix (prf ^ Long_Name.separator) thy))
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   557
                                    (thms_of_thy prf))
26706
4ea64590d28b replaced token translations by common markup;
wenzelm
parents: 26622
diff changeset
   558
    in
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   559
        case (thyname,objtype) of
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   560
           (NONE, NONE) =>
26613
725a3d9011d1 ThyInfo.get_names;
wenzelm
parents: 26603
diff changeset
   561
           setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   562
         | (NONE, SOME ObjFile) =>
26613
725a3d9011d1 ThyInfo.get_names;
wenzelm
parents: 26603
diff changeset
   563
           setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   564
         | (SOME fi, SOME ObjFile) =>
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   565
           setids (idtable ObjTheory (SOME fi) [fi])       (* TODO: check exists *)
22225
30ab97554602 Fix tell_thm_deps to match changse in PureThy.
aspinall
parents: 22216
diff changeset
   566
         | (NONE, SOME ObjTheory) =>
26613
725a3d9011d1 ThyInfo.get_names;
wenzelm
parents: 26603
diff changeset
   567
           setids (idtable ObjTheory NONE (ThyInfo.get_names()))
22225
30ab97554602 Fix tell_thm_deps to match changse in PureThy.
aspinall
parents: 22216
diff changeset
   568
         | (SOME thy, SOME ObjTheory) =>
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   569
           setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   570
         | (SOME thy, SOME ObjTheorem) =>
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   571
           setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   572
         | (NONE, SOME ObjTheorem) =>
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   573
           (* A large query, but not unreasonable. ~5000 results for HOL.*)
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   574
           (* Several setids should be allowed, but Eclipse code is currently broken:
23226
441f8a0bd766 removed obsolete Library.seq;
wenzelm
parents: 23178
diff changeset
   575
              List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
26613
725a3d9011d1 ThyInfo.get_names;
wenzelm
parents: 26603
diff changeset
   576
                         (ThyInfo.get_names()) *)
22225
30ab97554602 Fix tell_thm_deps to match changse in PureThy.
aspinall
parents: 22216
diff changeset
   577
           setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
26613
725a3d9011d1 ThyInfo.get_names;
wenzelm
parents: 26603
diff changeset
   578
                           (maps qualified_thms_of_thy (ThyInfo.get_names())))
22225
30ab97554602 Fix tell_thm_deps to match changse in PureThy.
aspinall
parents: 22216
diff changeset
   579
         | _ => warning ("askids: ignored argument combination")
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   580
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   581
27177
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   582
end;
adefd3454174 sane versions of (qualified_)thms_of_thy;
wenzelm
parents: 26939
diff changeset
   583
22159
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   584
fun askrefs (Askrefs vs) =
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   585
    let
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   586
        val url = #url vs            (* ask for references of a file (i.e. immediate pre-requisites) *)
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   587
        val thyname = #thyname vs    (* ask for references of a theory (other theories) *)
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   588
        val objtype = #objtype vs    (* ask for references of a particular type... *)
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   589
        val name = #name vs          (*   ... with this name *)
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   590
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   591
        fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   592
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   593
        val thy_name = Path.implode o #1 o Path.split_ext o Path.base
22159
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   594
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   595
        fun filerefs f =
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   596
            let val thy = thy_name f
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24079
diff changeset
   597
                val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy)
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   598
            in
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   599
                issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   600
                                     name=NONE, idtables=[], fileurls=filerefs})
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   601
            end
22159
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   602
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   603
        fun thyrefs thy =
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24079
diff changeset
   604
            let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy)
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   605
            in
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   606
                issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   607
                                     name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   608
                                                           ids=thyrefs}], fileurls=[]})
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   609
            end
22159
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   610
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   611
        fun thmrefs thmname =
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   612
            let
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   613
                (* TODO: interim: this is probably not right.
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   614
                   What we want is mapping onto simple PGIP name/context model. *)
26603
410d02ea13c9 moved global Toplevel state to structure Isar;
wenzelm
parents: 26552
diff changeset
   615
                val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
33030
wenzelm
parents: 32966
diff changeset
   616
                val thy = ProofContext.theory_of ctx
26343
0dd2eab7b296 simplified get_thm(s): back to plain name argument;
wenzelm
parents: 26336
diff changeset
   617
                val ths = [PureThy.get_thm thy thmname]
28809
7c2e1bbf3c36 retrieve thm deps from proof_body;
wenzelm
parents: 28588
diff changeset
   618
                val deps = #2 (thms_deps ths);
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   619
            in
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   620
                if null deps then ()
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   621
                else issue_pgip (Setrefs {url=url, thyname=thyname, name=name,
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   622
                                          objtype=SOME PgipTypes.ObjTheorem,
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   623
                                          idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem,
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   624
                                                     ids=deps}], fileurls=[]})
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   625
            end
22159
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   626
    in
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   627
        case (url,thyname,objtype,name) of
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   628
            (SOME file, NONE, _, _)  => filerefs file
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   629
          | (_,SOME thy,_,_)         => thyrefs thy
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   630
          | (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname
22159
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   631
          | _  => error ("Unimplemented/invalid case of <askrefs>")
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   632
    end
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   633
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   634
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   635
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   636
fun showid (Showid vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   637
    let
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   638
        val thyname = #thyname vs
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   639
        val objtype = #objtype vs
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   640
        val name = #name vs
22337
d4599c206446 Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents: 22249
diff changeset
   641
26603
410d02ea13c9 moved global Toplevel state to structure Isar;
wenzelm
parents: 26552
diff changeset
   642
        val topthy = Toplevel.theory_of o Isar.state
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   643
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22408
diff changeset
   644
        fun splitthy id =
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 29635
diff changeset
   645
            let val comps = Long_Name.explode id
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22408
diff changeset
   646
            in case comps of
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22408
diff changeset
   647
                   (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22408
diff changeset
   648
                 | [plainid] => (topthy(),plainid)
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22408
diff changeset
   649
                 | _ => raise Toplevel.UNDEF (* assert false *)
26706
4ea64590d28b replaced token translations by common markup;
wenzelm
parents: 26622
diff changeset
   650
            end
4ea64590d28b replaced token translations by common markup;
wenzelm
parents: 26622
diff changeset
   651
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   652
22337
d4599c206446 Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents: 22249
diff changeset
   653
        fun idvalue strings =
26706
4ea64590d28b replaced token translations by common markup;
wenzelm
parents: 26622
diff changeset
   654
            issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
23759
90bccef65004 Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents: 23723
diff changeset
   655
                                  text=[XML.Elem("pgml",[],
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   656
                                                 maps YXML.parse_body strings)] })
22337
d4599c206446 Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents: 22249
diff changeset
   657
32144
183c1010ac14 use regular Display.string_of_thm_global;
wenzelm
parents: 32091
diff changeset
   658
        fun strings_of_thm (thy, name) =
183c1010ac14 use regular Display.string_of_thm_global;
wenzelm
parents: 32091
diff changeset
   659
          map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
22337
d4599c206446 Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents: 22249
diff changeset
   660
33389
bb3a5fa94a91 modernized structure Proof_Display;
wenzelm
parents: 33030
diff changeset
   661
        val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   662
    in
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   663
        case (thyname, objtype) of
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   664
            (_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
22337
d4599c206446 Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents: 22249
diff changeset
   665
          | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
d4599c206446 Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents: 22249
diff changeset
   666
          | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   667
          | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   668
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   669
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   670
(*** Inspecting state ***)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   671
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   672
(* The file which is currently being processed interactively.
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   673
   In the pre-PGIP code, this was informed to Isabelle and the theory loader
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   674
   on completion, but that allows for circularity in case we read
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   675
   ourselves.  So PGIP opens the filename at the start of a script.
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   676
   We ought to prevent problems by modifying the theory loader to know
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   677
   about this special status, but for now we just keep a local reference.
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   678
*)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   679
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
   680
val currently_open_file = Unsynchronized.ref (NONE : pgipurl option)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   681
22163
a586b0af857e Expose currently open file
aspinall
parents: 22159
diff changeset
   682
fun get_currently_open_file () = ! currently_open_file;
a586b0af857e Expose currently open file
aspinall
parents: 22159
diff changeset
   683
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   684
fun askguise _ =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   685
    (* The "guise" is the PGIP abstraction of the prover's state.
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   686
       The <informguise> message is merely used for consistency checking. *)
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   687
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   688
        val openfile = !currently_open_file
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   689
26603
410d02ea13c9 moved global Toplevel state to structure Isar;
wenzelm
parents: 26552
diff changeset
   690
        val topthy = Toplevel.theory_of o Isar.state
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   691
        val topthy_name = Context.theory_name o topthy
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   692
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   693
        val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   694
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   695
        fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   696
        val openproofpos = topproofpos()
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   697
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   698
        issue_pgip (Informguise { file = openfile,
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   699
                                  theory = opentheory,
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   700
                                  (* would be nice to get thm name... *)
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   701
                                  theorem = NONE,
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   702
                                  proofpos = openproofpos })
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   703
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   704
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   705
fun parsescript (Parsescript vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   706
    let
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   707
        val text = #text vs
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   708
        val systemdata = #systemdata vs
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   709
        val location = #location vs   (* TODO: extract position *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   710
28020
1ff5167592ba get rid of tabs;
wenzelm
parents: 27865
diff changeset
   711
        val doc = PgipParser.pgip_parser Position.none text
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   712
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   713
        val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   714
        val locattrs = PgipTypes.attrs_of_location location
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   715
     in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   716
        issue_pgip (Parseresult { attrs= sysattrs@locattrs,
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   717
                                  doc = doc,
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
   718
                                  errs = [] })
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   719
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   720
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   721
fun showproofstate _ = isarcmd "pr"
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   722
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   723
fun showctxt _ = isarcmd "print_context"
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   724
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   725
fun searchtheorems (Searchtheorems vs) =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   726
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   727
        val arg = #arg vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   728
    in
21969
a8bf1106cb7c removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   729
        isarcmd ("find_theorems " ^ arg)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   730
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   731
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   732
fun setlinewidth (Setlinewidth vs) =
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   733
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   734
        val width = #width vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   735
    in
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   736
        isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   737
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   738
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   739
fun viewdoc (Viewdoc vs) =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   740
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   741
        val arg = #arg vs
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   742
    in
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28443
diff changeset
   743
        isarcmd ("print_" ^ arg)   (* FIXME: isabelle doc?.  Return URLs, maybe? *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   744
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   745
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   746
(*** Theory ***)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   747
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   748
fun doitem (Doitem vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   749
    let
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   750
        val text = #text vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   751
    in
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   752
        isarcmd text
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   753
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   754
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   755
fun undoitem _ =
21972
1b68312c4cf0 Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents: 21970
diff changeset
   756
    isarcmd "undo"
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   757
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   758
fun redoitem _ =
21972
1b68312c4cf0 Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents: 21970
diff changeset
   759
    isarcmd "redo"
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   760
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   761
fun aborttheory _ =
21972
1b68312c4cf0 Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents: 21970
diff changeset
   762
    isarcmd "kill"  (* was: "init_toplevel" *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   763
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   764
fun retracttheory (Retracttheory vs) =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   765
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   766
        val thyname = #thyname vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   767
    in
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   768
        isarcmd ("kill_thy " ^ quote thyname)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   769
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   770
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   771
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   772
(*** Files ***)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   773
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   774
(* Path management: we allow theory files to have dependencies in
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   775
   their own directory, but when we change directory for a new file we
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   776
   remove the path.  Leaving it there can cause confusion with
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   777
   difference in batch mode.
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   778
   NB: PGIP does not assume that the prover has a load path.
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   779
*)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   780
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   781
local
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
   782
    val current_working_dir = Unsynchronized.ref (NONE : string option)
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   783
in
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   784
fun changecwd_dir newdirpath =
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   785
   let
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   786
       val newdir = File.platform_path newdirpath
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   787
   in
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   788
       (case (!current_working_dir) of
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   789
            NONE => ()
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   790
          | SOME dir => ThyLoad.del_path dir;
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   791
        ThyLoad.add_path newdir;
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   792
        current_working_dir := SOME newdir)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   793
   end
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   794
end
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   795
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   796
fun changecwd (Changecwd vs) =
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   797
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   798
        val url = #url vs
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   799
        val newdir = PgipTypes.path_of_pgipurl url
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   800
    in
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   801
        changecwd_dir url
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   802
    end
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   803
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   804
fun openfile (Openfile vs) =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   805
  let
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   806
      val url = #url vs
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   807
      val filepath = PgipTypes.path_of_pgipurl url
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   808
      val filedir = Path.dir filepath
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   809
      val thy_name = Path.implode o #1 o Path.split_ext o Path.base
32966
5b21661fe618 indicate CRITICAL nature of various setmp combinators;
wenzelm
parents: 32738
diff changeset
   810
      val openfile_retract = Output.no_warnings_CRITICAL
5b21661fe618 indicate CRITICAL nature of various setmp combinators;
wenzelm
parents: 32738
diff changeset
   811
        (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   812
  in
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   813
      case !currently_open_file of
22028
c13f6b5bf2b8 Be more chatty in PGIP file operations.
aspinall
parents: 22014
diff changeset
   814
          SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   815
                                PgipTypes.string_of_pgipurl url)
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   816
        | NONE => (openfile_retract filepath;
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   817
                   changecwd_dir filedir;
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   818
                   priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   819
                   currently_open_file := SOME url)
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   820
  end
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   821
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   822
fun closefile _ =
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   823
    case !currently_open_file of
22042
64f8f5433f30 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents: 22028
diff changeset
   824
        SOME f => (proper_inform_file_processed f (Isar.state());
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   825
                   priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   826
                   currently_open_file := NONE)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   827
      | NONE => raise PGIP ("<closefile> when no file is open!")
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   828
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   829
fun loadfile (Loadfile vs) =
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   830
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   831
        val url = #url vs
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   832
    in
22171
58f554f51f0d Let <loadfile> execute even while a file is open interactively.
aspinall
parents: 22163
diff changeset
   833
        (* da: this doesn't seem to cause a problem, batch loading uses
58f554f51f0d Let <loadfile> execute even while a file is open interactively.
aspinall
parents: 22163
diff changeset
   834
           a different state context.  Of course confusion is still possible,
58f554f51f0d Let <loadfile> execute even while a file is open interactively.
aspinall
parents: 22163
diff changeset
   835
           e.g. file loaded depends on open file which is not yet saved. *)
58f554f51f0d Let <loadfile> execute even while a file is open interactively.
aspinall
parents: 22163
diff changeset
   836
        (* case !currently_open_file of
22028
c13f6b5bf2b8 Be more chatty in PGIP file operations.
aspinall
parents: 22014
diff changeset
   837
            SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   838
                                  PgipTypes.string_of_pgipurl url)
22171
58f554f51f0d Let <loadfile> execute even while a file is open interactively.
aspinall
parents: 22163
diff changeset
   839
          | NONE => *)
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   840
        use_thy_or_ml_file (File.platform_path url)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   841
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   842
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   843
fun abortfile _ =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   844
    case !currently_open_file of
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   845
        SOME f => (isarcmd "init_toplevel";
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   846
                   priority ("Aborted working in file: " ^
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   847
                             PgipTypes.string_of_pgipurl f);
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   848
                   currently_open_file := NONE)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   849
      | NONE => raise PGIP ("<abortfile> when no file is open!")
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   850
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   851
fun retractfile (Retractfile vs) =
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   852
    let
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   853
        val url = #url vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   854
    in
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   855
        case !currently_open_file of
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   856
            SOME f => raise PGIP ("<retractfile> when a file is open!")
22028
c13f6b5bf2b8 Be more chatty in PGIP file operations.
aspinall
parents: 22014
diff changeset
   857
          | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   858
                     (* TODO: next should be in thy loader, here just for testing *)
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   859
                     let
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   860
                         val name = thy_name url
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   861
                     in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end;
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   862
                     inform_file_retracted url)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   863
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   864
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   865
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   866
(*** System ***)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   867
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   868
fun systemcmd (Systemcmd vs) =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   869
  let
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   870
      val arg = #arg vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   871
  in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   872
      isarcmd arg
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   873
  end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   874
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   875
exception PGIP_QUIT;
23834
ad6ad61332fa avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents: 23801
diff changeset
   876
fun quitpgip _ = raise PGIP_QUIT
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   877
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   878
fun process_input inp = case inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   879
 of Pgip.Askpgip _          => askpgip inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   880
  | Pgip.Askpgml _          => askpgml inp
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   881
  | Pgip.Askprefs _         => askprefs inp
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   882
  | Pgip.Askconfig _        => askconfig inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   883
  | Pgip.Getpref _          => getpref inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   884
  | Pgip.Setpref _          => setpref inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   885
  | Pgip.Proverinit _       => proverinit inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   886
  | Pgip.Proverexit _       => proverexit inp
22408
3878265f4924 Simplify print mode. Support setproverflag.
aspinall
parents: 22397
diff changeset
   887
  | Pgip.Setproverflag _    => setproverflag inp
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   888
  | Pgip.Dostep _           => dostep inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   889
  | Pgip.Undostep _         => undostep inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   890
  | Pgip.Redostep _         => redostep inp
23435
061f28854017 Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents: 23226
diff changeset
   891
  | Pgip.Forget _           => error "<forget> not implemented by Isabelle"
061f28854017 Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents: 23226
diff changeset
   892
  | Pgip.Restoregoal _      => error "<restoregoal> not implemented by Isabelle"
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   893
  | Pgip.Abortgoal _        => abortgoal inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   894
  | Pgip.Askids _           => askids inp
22159
0cf0d3912239 Comment
aspinall
parents: 22042
diff changeset
   895
  | Pgip.Askrefs _          => askrefs inp
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   896
  | Pgip.Showid _           => showid inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   897
  | Pgip.Askguise _         => askguise inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   898
  | Pgip.Parsescript _      => parsescript inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   899
  | Pgip.Showproofstate _   => showproofstate inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   900
  | Pgip.Showctxt _         => showctxt inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   901
  | Pgip.Searchtheorems _   => searchtheorems inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   902
  | Pgip.Setlinewidth _     => setlinewidth inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   903
  | Pgip.Viewdoc _          => viewdoc inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   904
  | Pgip.Doitem _           => doitem inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   905
  | Pgip.Undoitem _         => undoitem inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   906
  | Pgip.Redoitem _         => redoitem inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   907
  | Pgip.Aborttheory _      => aborttheory inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   908
  | Pgip.Retracttheory _    => retracttheory inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   909
  | Pgip.Loadfile _         => loadfile inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   910
  | Pgip.Openfile _         => openfile inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   911
  | Pgip.Closefile _        => closefile inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   912
  | Pgip.Abortfile _        => abortfile inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   913
  | Pgip.Retractfile _      => retractfile inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   914
  | Pgip.Changecwd _        => changecwd inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   915
  | Pgip.Systemcmd _        => systemcmd inp
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21885
diff changeset
   916
  | Pgip.Quitpgip _         => quitpgip inp
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   917
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   918
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   919
fun process_pgip_element pgipxml =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   920
    case pgipxml of
21969
a8bf1106cb7c removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   921
        xml as (XML.Elem elem) =>
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   922
        (case Pgip.input elem of
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   923
             NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
26541
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 26463
diff changeset
   924
                              (XML.string_of xml))
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   925
           | SOME inp => (process_input inp)) (* errors later; packet discarded *)
21969
a8bf1106cb7c removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   926
      | XML.Text t => ignored_text_warning t
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   927
and ignored_text_warning t =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   928
    if size (Symbol.strip_blanks t) > 0 then
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   929
           warning ("Ignored text in PGIP packet: \n" ^ t)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   930
    else ()
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   931
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   932
fun process_pgip_tree xml =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   933
    (pgip_refid := NONE;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   934
     pgip_refseq := NONE;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   935
     (case xml of
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   936
          XML.Elem ("pgip", attrs, pgips) =>
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   937
          (let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   938
               val class = PgipTypes.get_attr "class" attrs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   939
               val dest  = PgipTypes.get_attr_opt "destid" attrs
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   940
               val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   941
               (* Respond to prover broadcasts, or messages for us. Ignore rest *)
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   942
               val processit =
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   943
                   case dest of
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   944
                       NONE =>    class = "pa"
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   945
                     | SOME id => matching_pgip_id id
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   946
           in if processit then
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   947
                  (pgip_refid :=  PgipTypes.get_attr_opt "id" attrs;
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   948
                   pgip_refseq := SOME seq;
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   949
                   List.app process_pgip_element pgips;
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   950
                   (* return true to indicate <ready/> *)
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   951
                   true)
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   952
              else
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   953
                  (* no response to ignored messages. *)
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   954
                  false
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   955
           end)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   956
        | _ => raise PGIP "Invalid PGIP packet received")
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   957
     handle PGIP msg =>
36148
4ddcc2b07891 spelling;
wenzelm
parents: 33389
diff changeset
   958
            (Output.error_msg ((msg ^ "\nPGIP error occurred in XML text below:\n") ^
26541
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 26463
diff changeset
   959
                               (XML.string_of xml));
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   960
             true))
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   961
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
   962
(* External input *)
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
   963
26541
14b268974c4b XML.string_of, XML.parse;
wenzelm
parents: 26463
diff changeset
   964
val process_pgip_plain = K () o process_pgip_tree o XML.parse
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   965
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   966
(* PGIP loop: process PGIP input only *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   967
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   968
local
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   969
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   970
exception XML_PARSE
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   971
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   972
fun loop ready src =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   973
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   974
        val _ = if ready then issue_pgip (Ready ()) else ()
21969
a8bf1106cb7c removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   975
        val pgipo =
a8bf1106cb7c removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   976
          (case try Source.get_single src of
a8bf1106cb7c removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   977
            SOME pgipo => pgipo
a8bf1106cb7c removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   978
          | NONE => raise XML_PARSE)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   979
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   980
        case pgipo of
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   981
             NONE  => ()
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   982
           | SOME (pgip,src') =>
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   983
             let
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   984
                 val ready' = (process_pgip_tree pgip)
22337
d4599c206446 Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents: 22249
diff changeset
   985
                                handle PGIP_QUIT => raise PGIP_QUIT
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22408
diff changeset
   986
                                     | e => (handler (e,SOME src'); true)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   987
             in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   988
                 loop ready' src'
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   989
             end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   990
    end handle e => handler (e,SOME src)  (* error in XML parse or Ready issue *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   991
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   992
and handler (e,srco) =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   993
    case (e,srco) of
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   994
        (XML_PARSE,SOME src) =>
22699
938c1011ac94 removed unused Output.panic hook -- internal to PG wrapper;
wenzelm
parents: 22678
diff changeset
   995
        panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
28443
de653f1ad78b more robust treatment of Interrupt (cf. exn.ML);
wenzelm
parents: 28375
diff changeset
   996
      | (Exn.Interrupt,SOME src) =>
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   997
        (Output.error_msg "Interrupt during PGIP processing"; loop true src)
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   998
      | (Toplevel.UNDEF,SOME src) =>
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
   999
        (Output.error_msg "No working context defined"; loop true src)
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
  1000
      | (e,SOME src) =>
31478
5e412e4c6546 ML_Compiler.exn_message;
wenzelm
parents: 30723
diff changeset
  1001
        (Output.error_msg (ML_Compiler.exn_message e); loop true src)
22337
d4599c206446 Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents: 22249
diff changeset
  1002
      | (PGIP_QUIT,_) => ()
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1003
      | (_,NONE) => ()
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1004
in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1005
  (* TODO: add socket interface *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1006
26552
5677b4faf295 renamed XML.parse_comment_whspc to XML.parse_comments;
wenzelm
parents: 26548
diff changeset
  1007
  val xmlP = XML.parse_comments |-- XML.parse_element >> single
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1008
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1009
  val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1010
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1011
  fun pgip_toplevel x = loop true x
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1012
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1013
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1014
21972
1b68312c4cf0 Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents: 21970
diff changeset
  1015
(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1016
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
  1017
fun init_outer_syntax () =
21972
1b68312c4cf0 Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents: 21970
diff changeset
  1018
  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
1b68312c4cf0 Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents: 21970
diff changeset
  1019
    (OuterParse.text >> (Toplevel.no_timing oo
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1020
      (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1021
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1022
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1023
(* init *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1024
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
  1025
val initialized = Unsynchronized.ref false;
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1026
22699
938c1011ac94 removed unused Output.panic hook -- internal to PG wrapper;
wenzelm
parents: 22678
diff changeset
  1027
fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
21969
a8bf1106cb7c removed conditional combinator;
wenzelm
parents: 21959
diff changeset
  1028
  | init_pgip true =
a8bf1106cb7c removed conditional combinator;
wenzelm
parents: 21959
diff changeset
  1029
      (! initialized orelse
25445
01f3686f4304 Init outer syntax after message setup to avoid spurious output.
aspinall
parents: 25275
diff changeset
  1030
        (setup_preferences_tweak ();
28037
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
  1031
         Output.add_mode proof_generalN Output.default_output Output.default_escape;
915b9a777441 changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents: 28020
diff changeset
  1032
         Markup.add_mode proof_generalN YXML.output_markup;
25445
01f3686f4304 Init outer syntax after message setup to avoid spurious output.
aspinall
parents: 25275
diff changeset
  1033
         setup_messages ();
32966
5b21661fe618 indicate CRITICAL nature of various setmp combinators;
wenzelm
parents: 32738
diff changeset
  1034
         Output.no_warnings_CRITICAL init_outer_syntax ();
25445
01f3686f4304 Init outer syntax after message setup to avoid spurious output.
aspinall
parents: 25275
diff changeset
  1035
         setup_thy_loader ();
01f3686f4304 Init outer syntax after message setup to avoid spurious output.
aspinall
parents: 25275
diff changeset
  1036
         setup_present_hook ();
01f3686f4304 Init outer syntax after message setup to avoid spurious output.
aspinall
parents: 25275
diff changeset
  1037
         init_pgip_session_id ();
01f3686f4304 Init outer syntax after message setup to avoid spurious output.
aspinall
parents: 25275
diff changeset
  1038
         welcome ();
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
  1039
         Unsynchronized.set initialized);
21969
a8bf1106cb7c removed conditional combinator;
wenzelm
parents: 21959
diff changeset
  1040
        sync_thy_loader ();
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
  1041
       Unsynchronized.change print_mode (update (op =) proof_generalN);
21969
a8bf1106cb7c removed conditional combinator;
wenzelm
parents: 21959
diff changeset
  1042
       pgip_toplevel tty_src);
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1043
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1044
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1045
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1046
(** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1047
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1048
local
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32144
diff changeset
  1049
    val pgip_output_channel = Unsynchronized.ref Output.writeln_default
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1050
in
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1051
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1052
(* Set recipient for PGIP results *)
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1053
fun init_pgip_channel writefn =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
  1054
    (init_pgip_session_id();
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
  1055
     pgip_output_channel := writefn)
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1056
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
  1057
(* Process a PGIP command.
fbd068dd4d29 minor tuning;
wenzelm
parents: 21902
diff changeset
  1058
   This works for preferences but not generally guaranteed
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1059
   because we haven't done full setup here (e.g., no pgml mode)  *)
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1060
fun process_pgip str =
32966
5b21661fe618 indicate CRITICAL nature of various setmp combinators;
wenzelm
parents: 32738
diff changeset
  1061
     setmp_CRITICAL output_xml_fn (!pgip_output_channel) process_pgip_plain str
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1062
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21646
diff changeset
  1063
end
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1064
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
  1065
end;