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