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