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