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