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