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