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