src/Pure/proof_general.ML
author aspinall
Thu Sep 15 10:33:35 2005 +0200 (2005-09-15)
changeset 17403 de60322ff13a
parent 17314 04e21a27c0ad
child 17407 38e0219ec022
permissions -rw-r--r--
Change PGIP attribute name class->messageclass to avoid Java keyword clash.
     1 (*  Title:      Pure/proof_general.ML
     2     ID:         $Id$
     3     Author:     David Aspinall and Markus Wenzel
     4 
     5 Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk)
     6 Includes support for PGIP control language for Isabelle/Isar.
     7 
     8 ===========================================================================
     9 NOTE: With this version you will lose support for the Isabelle
    10 settings menu in the currently released version of Proof General (3.5).
    11 No other changes should be visible in the Emacs interface.
    12 
    13 The 3.6pre pre-release versions of Emacs Proof General now support the
    14 new PGIP format for preferences and restore the settings menu.
    15 Please visit http://proofgeneral.inf.ed.ac.uk/develdownload
    16 ===========================================================================
    17 
    18 STATUS: this version is an experimental version that supports PGIP 2.X.
    19 *)
    20 
    21 signature PROOF_GENERAL =
    22 sig
    23   val update_thy_only: string -> unit
    24   val try_update_thy_only: string -> unit
    25   val inform_file_retracted: string -> unit
    26   val inform_file_processed: string -> unit
    27   val preferences:
    28       (string *
    29         (string *
    30          (string *
    31           (string * (string * (unit -> string)) *
    32            (string -> unit)))) list) list ref
    33   val process_pgip: string -> unit
    34   val thms_containing: string list -> unit
    35   val help: unit -> unit
    36   val show_context: unit -> theory
    37   val kill_goal: unit -> unit
    38   val repeat_undo: int -> unit
    39   val isa_restart: unit -> unit
    40   val full_proofs: bool -> unit
    41   val isarcmd: string -> unit
    42   val init: bool -> unit
    43   val init_pgip: bool -> unit
    44   val write_keywords: string -> unit
    45   val xmls_of_str: string -> string list   (*temp for testing parser*)
    46 end;
    47 
    48 structure ProofGeneral: PROOF_GENERAL =
    49 struct
    50 
    51 structure P = OuterParse;
    52 
    53 
    54 (* PGIP messaging mode (independent of PGML output) *)
    55 
    56 val pgip_active = ref false;
    57 val pgip_emacs_compatibility_flag = ref false;
    58 
    59 fun pgip () = (! pgip_active);
    60 fun pgip_emacs_compatibility () = (! pgip_emacs_compatibility_flag);
    61 
    62 
    63 (* print modes *)
    64 
    65 val proof_generalN = "ProofGeneral";  (*token markup (colouring vars, etc.)*)
    66 val pgasciiN = "PGASCII";             (*plain 7-bit ASCII communication*)
    67 val xsymbolsN = Symbol.xsymbolsN;     (*X-Symbol symbols*)
    68 val pgmlN = "PGML";                   (*XML escapes and PGML symbol elements*)
    69 val pgmlatomsN = "PGMLatoms";         (*variable kind decorations*)
    70 val thm_depsN = "thm_deps";           (*meta-information about theorem deps*)
    71 
    72 fun pgml () = Output.has_mode pgmlN;
    73 
    74 fun special oct =
    75   if Output.has_mode pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
    76   else oct_char oct;
    77 
    78 
    79 (* text output: print modes for xsymbol and PGML *)
    80 
    81 local
    82 
    83 fun xsym_output "\\" = "\\\\"
    84   | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
    85 
    86 fun xsymbols_output s =
    87   if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then
    88     let val syms = Symbol.explode s
    89     in (implode (map xsym_output syms), real (Symbol.length syms)) end
    90   else Symbol.default_output s;
    91 
    92 fun pgml_sym s =
    93   (case Symbol.decode s of
    94     (*NB: an alternative here would be to output the default print mode alternative
    95       in the element content, but unfortunately print modes are not that fine grained.*)
    96     Symbol.Char s => XML.text s
    97   | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
    98   | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *)
    99   | Symbol.Raw s => s);
   100 
   101 fun pgml_output str =
   102   let val syms = Symbol.explode str
   103   in (implode (map pgml_sym syms), real (Symbol.length syms)) end;
   104 
   105 in
   106 
   107 fun setup_xsymbols_output () =
   108   Output.add_mode xsymbolsN
   109     (xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
   110 
   111 fun setup_pgml_output () =
   112   Output.add_mode pgmlN
   113     (pgml_output, Symbol.default_indent, Symbol.encode_raw);
   114 
   115 end;
   116 
   117 
   118 (* token translations *)
   119 
   120 local
   121 
   122 fun end_tag () = special "350";
   123 val class_tag = ("class", fn () => special "351");
   124 val tfree_tag = ("tfree", fn () => special "352");
   125 val tvar_tag = ("tvar", fn () => special "353");
   126 val free_tag = ("free", fn () => special "354");
   127 val bound_tag = ("bound", fn () => special "355");
   128 val var_tag = ("var", fn () => special "356");
   129 val skolem_tag = ("skolem", fn () => special "357");
   130 
   131 fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
   132 
   133 fun tagit (kind, bg_tag) x =
   134  (if Output.has_mode pgmlatomsN then xml_atom kind x
   135   else bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
   136 
   137 fun free_or_skolem x =
   138   (case try Syntax.dest_skolem x of
   139     NONE => tagit free_tag x
   140   | SOME x' => tagit skolem_tag x');
   141 
   142 fun var_or_skolem s =
   143   (case Syntax.read_variable s of
   144     SOME (x, i) =>
   145       (case try Syntax.dest_skolem x of
   146         NONE => tagit var_tag s
   147       | SOME x' => tagit skolem_tag
   148           (setmp show_question_marks true Syntax.string_of_vname (x', i)))
   149   | NONE => tagit var_tag s);
   150 
   151 val proof_general_trans =
   152  Syntax.tokentrans_mode proof_generalN
   153   [("class", tagit class_tag),
   154    ("tfree", tagit tfree_tag),
   155    ("tvar", tagit tvar_tag),
   156    ("free", free_or_skolem),
   157    ("bound", tagit bound_tag),
   158    ("var", var_or_skolem)];
   159 
   160 in
   161 
   162 val _ = Context.add_setup [Theory.add_tokentrfuns proof_general_trans];
   163 
   164 end;
   165 
   166 
   167 (* assembling PGIP packets *)
   168 
   169 val pgip_refid  = ref NONE: string option ref;
   170 val pgip_refseq = ref NONE: string option ref;
   171 
   172 local
   173   val pgip_class  = "pg"
   174   val pgip_tag = "Isabelle/Isar"
   175   val pgip_id = ref ""
   176   val pgip_seq = ref 0
   177   fun pgip_serial () = inc pgip_seq
   178 
   179   fun assemble_pgips pgips =
   180     XML.element
   181       "pgip"
   182       ([("tag",    pgip_tag),
   183         ("messageclass",  pgip_class),
   184         ("seq",    string_of_int (pgip_serial())),
   185         ("id",     !pgip_id)] @
   186        if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
   187        (* destid=refid since Isabelle only communicates back to sender,
   188           so we may omit refid from attributes.
   189        if_none (Option.map (single o (pair "refid"))  (! pgip_refid)) [] @
   190        *)
   191        if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) [])
   192       pgips;
   193 
   194 in
   195 
   196 fun init_pgip_session_id () =
   197     pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
   198                getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
   199 
   200 
   201 fun matching_pgip_id id = (id = !pgip_id)
   202 
   203 fun decorated_output bg en prfx =
   204   writeln_default o enclose bg en o prefix_lines prfx;
   205 
   206 (* FIXME: see Rev 1.48 [PG CVS] for cleaner version of this which can be used
   207    for PG 4.0 which processes PGIP without needing special chars *)
   208 fun issue_pgips ps =
   209   if pgip_emacs_compatibility() then
   210     decorated_output (*add urgent message annotation*)
   211       (special "360") (special "361") ""
   212       (assemble_pgips ps)
   213   else
   214     writeln_default (assemble_pgips ps);
   215 
   216 fun assemble_pgip resp attrs s = assemble_pgips [XML.element resp attrs [s]];
   217 fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []];
   218 
   219 (* FIXME: need to add stuff to gather PGIPs here *)
   220 fun issue_pgip resp attrs txt =
   221   if pgip_emacs_compatibility () then
   222     decorated_output (*add urgent message annotation*)
   223       (special "360") (special "361") ""
   224       (assemble_pgip resp attrs txt)
   225   else
   226     writeln_default (assemble_pgip resp attrs txt);
   227 
   228 (* FIXME: temporarily to support PG 3.4 *)
   229 fun issue_pgip_maybe_decorated bg en resp attrs s =
   230   if pgip_emacs_compatibility () then
   231     (*in PGIP mode, but using escape characters as well*)
   232     writeln_default (enclose bg en (assemble_pgip resp attrs s))
   233   else
   234     issue_pgip resp attrs s;
   235 
   236 fun issue_pgipe resp attrs = writeln_default (assemble_pgipe resp attrs);
   237 
   238 end;
   239 
   240 
   241 (* messages and notification *)
   242 
   243 local
   244   val delay_msgs = ref false;   (*true: accumulate messages*)
   245   val delayed_msgs = ref [];
   246 in
   247 
   248 fun message resp attrs bg en prfx s =
   249   if pgip () then
   250    (if (! delay_msgs) then
   251       delayed_msgs := (resp, attrs, prefix_lines prfx s) :: ! delayed_msgs (*NB: no decs*)
   252     else
   253       issue_pgip_maybe_decorated bg en resp attrs
   254         (XML.element "pgmltext" [] [prefix_lines prfx s]))
   255   else decorated_output bg en prfx s;
   256 
   257 fun start_delay_msgs () = (set delay_msgs; delayed_msgs := []);
   258 
   259 fun end_delayed_msgs () = (reset delay_msgs;
   260   (! delayed_msgs) |> map (fn (resp, attrs, s) =>
   261     XML.element resp attrs [XML.element "pgmltext" [] [s]]));
   262 
   263 end;
   264 
   265 local
   266   val display_area = ("area", "display");
   267   val message_area = ("area", "message");
   268   val internal_category = ("messagecategory", "internal");
   269   val info_category = ("messagecategory", "information");
   270   val tracing_category = ("messagecategory", "tracing");
   271   val urgent_indication = ("urgent", "y");
   272   val nonfatal = ("fatality", "nonfatal");
   273   val fatal = ("fatality", "fatal");
   274   val panic = ("fatality", "panic");
   275 
   276   val thyname_attr = pair "thyname";
   277   val url_attr = pair "url";
   278   fun localfile_url_attr path = url_attr ("file:///" ^ path);
   279 in
   280 
   281 fun setup_messages () =
   282  (writeln_fn := (fn s => message "normalresponse" [message_area] "" "" "" s);
   283   priority_fn := (fn s => message "normalresponse" [message_area, urgent_indication]
   284     (special "360") (special "361") "" s);
   285   tracing_fn := (fn s => message "normalresponse"  [message_area, tracing_category]
   286     (special "360" ^ special "375") (special "361") "" s);
   287   info_fn := (fn s => message "normalresponse" [message_area, info_category]
   288     (special "362") (special "363") "+++ " s);
   289   debug_fn := (fn s => message "normalresponse" [message_area, internal_category]
   290     (special "362") (special "363") "+++ " s);
   291   warning_fn := (fn s => message "errorresponse" [nonfatal]
   292     (special "362") (special "363") "### " s);
   293   error_fn := (fn s => message "errorresponse" [fatal]
   294     (special "364") (special "365") "*** " s);
   295   panic_fn := (fn s => message "errorresponse" [panic]
   296     (special "364") (special "365") "!!! " s));
   297 
   298 
   299 (* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
   300 
   301 fun with_displaywrap (elt, attrs) dispfn =
   302   let
   303     val lines = ref ([]: string list);
   304     fun wlgrablines s = lines := s :: ! lines;
   305   in
   306     setmp writeln_fn wlgrablines dispfn ();
   307     (* IMPORTANT FIXME: XML.element here too inefficient, should use stream output *)
   308     issue_pgip elt attrs (XML.element "pgmltext" [] (! lines))
   309   end;
   310 
   311 fun emacs_notify s = decorated_output (special "360") (special "361") "" s;
   312 
   313 fun tell_clear_goals () =
   314   if pgip () then
   315     issue_pgipe "cleardisplay" [display_area]
   316   else
   317     emacs_notify "Proof General, please clear the goals buffer.";
   318 
   319 fun tell_clear_response () =
   320   if pgip () then
   321     issue_pgipe "cleardisplay" [message_area]
   322   else
   323     emacs_notify "Proof General, please clear the response buffer.";
   324 
   325 fun tell_file_loaded path =
   326   if pgip () then
   327     issue_pgipe "informfileloaded"
   328       [localfile_url_attr  (XML.text (File.platform_path path))]
   329   else
   330     emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
   331 
   332 fun tell_file_retracted path =
   333   if pgip() then
   334     issue_pgipe "informfileretracted"
   335       [localfile_url_attr  (XML.text (File.platform_path path))]
   336   else
   337     emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
   338 
   339 
   340 (* theory / proof state output *)
   341 
   342 local
   343 
   344 fun tmp_markers f =
   345   setmp Display.current_goals_markers (special "366", special "367", "") f ();
   346 
   347 fun statedisplay prts =
   348   issue_pgip "proofstate" []
   349     (XML.element "pgml" []
   350       [XML.element "statedisplay" [] [Pretty.output (Pretty.chunks prts)]]);
   351 
   352 fun print_current_goals n m st =
   353   if pgml () then statedisplay (Display.pretty_current_goals n m st)
   354   else tmp_markers (fn () => Display.print_current_goals_default n m st);
   355 
   356 fun print_state b st =
   357   if pgml () then statedisplay (Toplevel.pretty_state b st)
   358   else tmp_markers (fn () => Toplevel.print_state_default b st);
   359 
   360 in
   361 
   362 fun setup_state () =
   363   (Display.print_current_goals_fn := print_current_goals;
   364    Toplevel.print_state_fn := print_state;
   365    (* FIXME: check next octal char won't appear in pgip? *)
   366    Toplevel.prompt_state_fn := (fn s => suffix (special "372")
   367      (Toplevel.prompt_state_default s)));
   368 
   369 end;
   370 
   371 end;
   372 
   373 
   374 (* misc commands for ProofGeneral/isa *)
   375 
   376 fun thms_containing ss =
   377   FindTheorems.print_theorems (ProofContext.init (the_context ())) NONE NONE
   378     (map (fn s => (true, FindTheorems.Pattern s)) ss);
   379 
   380 val welcome = priority o Session.welcome;
   381 val help = welcome;
   382 val show_context = Context.the_context;
   383 
   384 fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
   385 
   386 fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
   387 
   388 fun repeat_undo 0 = ()
   389   | repeat_undo 1 = undo ()
   390   | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
   391 
   392 
   393 (* theory loader actions *)
   394 
   395 local
   396 
   397 fun add_master_files name files =
   398   let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
   399   in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
   400 
   401 fun trace_action action name =
   402   if action = ThyInfo.Update then
   403     List.app tell_file_loaded (ThyInfo.loaded_files name)
   404   else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
   405     List.app tell_file_retracted (add_master_files name (ThyInfo.loaded_files name))
   406   else ();
   407 
   408 in
   409   fun setup_thy_loader () = ThyInfo.add_hook trace_action;
   410   fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
   411 end;
   412 
   413 
   414 (* prepare theory context *)
   415 
   416 val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
   417 
   418 (* FIXME general treatment of tracing*)
   419 val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
   420 
   421 fun dynamic_context () =
   422   (case Context.get_context () of
   423     SOME thy => "  Using current (dynamic!) one: " ^ quote (Context.theory_name thy)
   424   | NONE => "");
   425 
   426 fun try_update_thy_only file =
   427   ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
   428     let val name = thy_name file in
   429       if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
   430       then update_thy_only name
   431       else warning ("Unkown theory context of ML file." ^ dynamic_context ())
   432     end) ();
   433 
   434 
   435 (* get informed about files *)
   436 
   437 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
   438 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
   439 val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
   440 
   441 fun proper_inform_file_processed file state =
   442   let val name = thy_name file in
   443     if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
   444      (ThyInfo.touch_child_thys name;
   445       transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
   446        (warning msg; warning ("Failed to register theory: " ^ quote name);
   447         tell_file_retracted (Path.base (Path.unpack file))))
   448     else raise Toplevel.UNDEF
   449   end;
   450 
   451 fun vacuous_inform_file_processed file state =
   452  (warning ("No theory " ^ quote (thy_name file));
   453   tell_file_retracted (Path.base (Path.unpack file)));
   454 
   455 
   456 (* restart top-level loop (keeps most state information) *)
   457 
   458 local
   459 
   460 fun restart isar =
   461  (if isar then tell_clear_goals () else kill_goal ();
   462   tell_clear_response ();
   463   welcome ());
   464 
   465 in
   466 
   467 fun isa_restart () = restart false;
   468 fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
   469 
   470 end;
   471 
   472 fun full_proofs true = proofs := 2
   473   | full_proofs false = proofs := 1;
   474 
   475 
   476 (* theorem dependency output *)
   477 
   478 local
   479 
   480 val spaces_quote = space_implode " " o map quote;
   481 
   482 (* FIXME: investigate why dependencies at the moment include themselves! *)
   483 fun thm_deps_message (thms, deps) =
   484   if pgip() then
   485     issue_pgips
   486       [XML.element
   487         "metainforesponse"  (* FIXME: get thy name from info here? *)
   488         [("infotype", "isabelle_theorem_dependencies")]
   489         [XML.element "value" [("name", "thms")] [XML.text thms],
   490          XML.element "value" [("name", "deps")] [XML.text deps]]]
   491   else emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
   492 
   493 fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
   494   let
   495     val names = filter_out (equal "") (map Thm.name_of_thm ths);
   496     val deps = filter_out (equal "")
   497       (Symtab.keys (fold Proofterm.thms_of_proof
   498         (map Thm.proof_of ths) Symtab.empty));
   499   in
   500     if null names orelse null deps then ()
   501     else thm_deps_message (spaces_quote names, spaces_quote deps)
   502   end);
   503 
   504 in
   505 
   506 fun setup_present_hook () =
   507   Present.add_hook (fn _ => fn res => tell_thm_deps (List.concat (map #2 res)));
   508 
   509 end;
   510 
   511 
   512 
   513 (** preferences **)
   514 
   515 local
   516 
   517 val pgipnat = XML.element "pgipint" [("min", "0")] [];
   518 fun pgipnatmax max = XML.element "pgipint" [("min", "0"), ("max", string_of_int max)] [];
   519 val pgipbool = XML.element "pgipbool" [] [];
   520 
   521 fun with_default f = (f (), f);
   522 
   523 in
   524 
   525 fun nat_option r = (pgipnat,
   526   with_default (fn () => string_of_int (! r)),
   527   (fn s => (case Syntax.read_nat s of
   528       NONE => error ("nat_option: illegal value: " ^ s)
   529     | SOME i => r := i)));
   530 
   531 fun bool_option r = (pgipbool,
   532   with_default (fn () => Bool.toString (! r)),
   533   (fn "false" => r := false | "true" => r := true
   534     | x => error ("bool_option: illegal value: " ^ x)));
   535 
   536 val proof_option = (pgipbool,
   537   with_default (fn () => Bool.toString (! proofs >= 2)),
   538   (fn "false" => proofs := 1 | "true" => proofs := 2
   539     | x => error ("proof_option: illegal value: " ^ x)));
   540 
   541 val thm_deps_option = (pgipbool,
   542   with_default (fn () => Bool.toString (Output.has_mode thm_depsN)),
   543   (fn "false" => change print_mode (remove (op =) thm_depsN)
   544     | "true" => change print_mode (insert (op =) thm_depsN)
   545     | x => error ("thm_deps_option: illegal value: " ^ x)));
   546 
   547 local
   548   val pg_print_depth_val = ref 10;
   549   fun pg_print_depth n = (print_depth n; pg_print_depth_val := n)
   550 in
   551 
   552 val print_depth_option = (pgipnat,
   553   with_default (fn () => string_of_int (! pg_print_depth_val)),
   554   (fn s => (case Syntax.read_nat s of
   555       NONE => error ("print_depth_option: illegal value: " ^ s)
   556     | SOME i => pg_print_depth i)));
   557 end;
   558 
   559 val preferences = ref
   560   [("Display",
   561     [("show-types",
   562       ("Include types in display of Isabelle terms",
   563        bool_option show_types)),
   564      ("show-sorts",
   565       ("Include sorts in display of Isabelle terms",
   566        bool_option show_sorts)),
   567      ("show-consts",
   568       ("Show types of consts in Isabelle goal display",
   569        bool_option show_consts)),
   570      ("long-names",
   571       ("Show fully qualified names in Isabelle terms",
   572        bool_option long_names)),
   573      ("show-brackets",
   574       ("Show full bracketing in Isabelle terms",
   575        bool_option show_brackets)),
   576      ("show-main-goal",
   577       ("Show main goal in proof state display",
   578        bool_option Proof.show_main_goal)),
   579      ("eta-contract",
   580       ("Print terms eta-contracted",
   581        bool_option Syntax.eta_contract))]),
   582    ("Advanced Display",
   583     [("goals-limit",
   584       ("Setting for maximum number of goals printed",
   585        nat_option goals_limit)),
   586      ("prems-limit",
   587       ("Setting for maximum number of premises printed",
   588        nat_option ProofContext.prems_limit)),
   589      ("print-depth",
   590       ("Setting for the ML print depth",
   591        print_depth_option)),
   592      ("show-question-marks",
   593       ("Show leading question mark of variable name",
   594        bool_option show_question_marks))]),
   595    ("Tracing",
   596     [("trace-simplifier",
   597       ("Trace simplification rules.",
   598        bool_option trace_simp)),
   599      ("trace-rules",
   600       ("Trace application of the standard rules",
   601        bool_option trace_rules)),
   602      ("trace-unification",
   603       ("Output error diagnostics during unification",
   604        bool_option Pattern.trace_unify_fail)),
   605      ("global-timing",
   606       ("Whether to enable timing in Isabelle.",
   607        bool_option Output.timing))]),
   608    ("Proof",
   609     [("quick-and-dirty",
   610       ("Take a few short cuts",
   611        bool_option quick_and_dirty)),
   612      ("full-proofs",
   613       ("Record full proof objects internally",
   614        proof_option)),
   615      ("theorem-dependencies",
   616        ("Track theorem dependencies within Proof General",
   617         thm_deps_option)),
   618      ("skip-proofs",
   619       ("Ignore proof scripts (interactive-only)",
   620        bool_option Toplevel.skip_proofs))])
   621    ];
   622 end;
   623 
   624 
   625 (* Configuration: GUI config, proverinfo messages *)
   626 
   627 local
   628     val config_file = "~~/lib/ProofGeneral/pgip_isar.xml"
   629     val name_attr = pair "name"
   630     val version_attr = pair "version"
   631     val isabelle_www = "http://isabelle.in.tum.de/"
   632 in
   633 fun send_pgip_config () =
   634     let
   635         val path = Path.unpack config_file
   636         val exists = File.exists path
   637         val proverinfo =
   638             XML.element "proverinfo"
   639               [("name",Session.name()), ("version", version),
   640                ("url", isabelle_www), ("filenameextns", ".thy;")]
   641             [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
   642              XML.element "helpdoc"
   643          (* NB: would be nice to generate/display docs from isatool
   644           doc, but that program may not be running on same machine;
   645           front end should be responsible for launching viewer, etc. *)
   646                       [("name", "Isabelle/HOL Tutorial"),
   647                        ("descr", "A Gentle Introduction to Isabelle/HOL"),
   648                        ("url",  "http://isabelle.in.tum.de/dist/Isabelle2004/doc/tutorial.pdf")]
   649               []]
   650     in
   651         if exists then
   652             (issue_pgips [proverinfo]; issue_pgips [File.read path])
   653         else panic ("PGIP configuration file " ^ config_file ^ " not found")
   654     end;
   655 end
   656 
   657 
   658 (* Reveal some information about prover state *)
   659 fun send_informguise (openfile, opentheory, openproofpos) =
   660     let val guisefile =
   661             case openfile of SOME f => [XML.element "guisefile"
   662                                                     [("url",Url.pack (Url.File (Path.unpack f)))] []]
   663                            | _ => []
   664         val guisetheory =
   665             case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
   666                              | _ => []
   667         val guiseproof =
   668             case openproofpos of SOME i => [XML.element "guiseproof" [("proofpos", string_of_int i)] []]
   669                                | _ => []
   670     in
   671         issue_pgips [XML.element "informguise" [] (guisefile @ guisetheory @ guiseproof)]
   672     end
   673 
   674 
   675 (* PGIP identifier tables (prover objects). [incomplete] *)
   676 
   677 local
   678     val objtype_thy  = "theory"
   679     val objtype_thm  = "theorem"
   680     val objtype_term = "term"
   681     val objtype_type = "type"
   682 
   683     fun xml_idtable ty ctx ids =
   684         let
   685             fun ctx_attr (SOME c)= [("context", c)]
   686               | ctx_attr NONE    = []
   687             fun xmlid x = XML.element "identifier" [] [XML.text x];
   688         in
   689             XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
   690                                   (map xmlid ids)
   691         end
   692 in
   693 
   694 fun setids t = issue_pgip "setids" [] t
   695 fun addids t = issue_pgip "addids" [] t
   696 fun delids t = issue_pgip "delids" [] t
   697 
   698 fun delallids ty = setids (xml_idtable ty NONE [])
   699 
   700 fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
   701 fun clear_thy_idtable () = delallids objtype_thy
   702 
   703 fun send_thm_idtable ctx thy =
   704     addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy)));
   705 
   706 fun clear_thm_idtable () = delallids objtype_thm
   707 
   708 (* fun send_type_idtable thy = TODO, it's a bit low-level messy
   709    & maybe not so useful anyway *)
   710 
   711 end
   712 
   713 (* Response to interface queries about known objects *)
   714 
   715 local
   716  val topthy = Toplevel.theory_of o Toplevel.get_state
   717  fun pthm thy name = print_thm (get_thm thy (Name name))
   718 
   719  fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
   720 in
   721 (* FIXME: add askids for "file" here, which returns single theory with same name *)
   722 fun askids (NONE, SOME "theory")  = send_thy_idtable NONE (ThyInfo.names())
   723   | askids (NONE, NONE) =  send_thy_idtable NONE (ThyInfo.names())
   724                            (* only theories known in top context *)
   725   | askids (SOME thy, SOME "theory") = send_thy_idtable (SOME thy) (ThyInfo.get_preds thy)
   726   | askids (SOME thy, SOME "theorem") = send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)
   727   | askids (SOME thy, NONE) = (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy);
   728                                send_thm_idtable (SOME thy) (ThyInfo.get_theory thy))
   729   | askids (_, SOME ot) = error ("No objects of type "^(quote ot)^" are available here.")
   730 
   731 fun showid (_,        "theory", n) =
   732     with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
   733   | showid (SOME thy, "theorem", t) =
   734     with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
   735   | showid (NONE,     "theorem", t) =
   736     with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t)
   737   | showid (_, ot, _) = error ("Cannot show objects of type "^ot)
   738 
   739 end
   740 
   741 
   742 (** Parsing proof scripts without execution **)
   743 
   744 (* Notes.
   745    This is quite tricky, because 1) we need to put back whitespace which
   746    was removed during parsing so we can provide markup around commands;
   747    2) parsing is intertwined with execution in Isar so we have to repeat
   748    the parsing to extract interesting parts of commands.  The trace of
   749    tokens parsed which is now recorded in each transition (added by
   750    Markus June '04) helps do this, but the mechanism is still a bad mess.
   751 
   752    If we had proper parse trees it would be easy, although having a
   753    fixed type of trees might be tricky with Isar's extensible parser.
   754 
   755    Probably the best solution is to produce the meta-information at
   756    the same time as the parse, for each command, e.g. by recording a
   757    list of (name,objtype) pairs which record the bindings created by
   758    a command.  This would require changing the interfaces in
   759    outer_syntax.ML (or providing new ones),
   760 
   761     datatype metainfo = Binding of string * string  (* name, objtype *)
   762 
   763     val command_withmetainfo: string -> string -> string ->
   764       (token list ->
   765        ((Toplevel.transition -> Toplevel.transition) * metainfo list) *
   766        token list) -> parser
   767 
   768    We'd also like to render terms as they appear in output, but this
   769    will be difficult because inner syntax is extensible and we don't
   770    have the correct syntax to hand when just doing outer parsing
   771    without execution.  A reasonable approximation could
   772    perhaps be obtained by using the syntax of the current context.
   773    However, this would mean more mess trying to pick out terms,
   774    so at this stage a more serious change to the Isar functions
   775    seems necessary.
   776 *)
   777 
   778 local
   779     fun markup_text str elt = [XML.element elt [] [XML.text str]]
   780     fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
   781     fun empty elt = [XML.element elt [] []]
   782 
   783     fun whitespace str = XML.element "whitespace" [] [XML.text str]
   784 
   785     (* an extra token is needed to terminate the command *)
   786     val sync = OuterSyntax.scan "\\<^sync>";
   787 
   788     fun named_item_elt_with nameattr toks str elt nameP objtyp =
   789         let
   790             val name = (fst (nameP (toks@sync)))
   791                         handle _ => (error ("Error occurred in name parser for " ^ elt ^
   792                                             "(objtype: " ^ objtyp ^ ")");
   793                                      "")
   794 
   795         in
   796             [XML.element elt
   797                          ((if name="" then [] else [(nameattr, name)])@
   798                           (if objtyp="" then [] else [("objtype", objtyp)]))
   799                          ([XML.text str])]
   800         end
   801 
   802     val named_item_elt = named_item_elt_with "name"
   803     val thmnamed_item_elt = named_item_elt_with "thmname"
   804 
   805     fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg)
   806 
   807     (* FIXME: allow dynamic extensions to language here: we need a hook in
   808        outer_syntax.ML to reset this table. *)
   809 
   810     val keywords_classification_table = ref (NONE: string Symtab.table option)
   811 
   812     fun get_keywords_classification_table () =
   813         case (!keywords_classification_table) of
   814           SOME t => t
   815         | NONE => (let
   816                      val tab = fold (fn (c, _, k, _) => Symtab.curried_update (c, k))
   817                                     (OuterSyntax.dest_parsers ()) Symtab.empty;
   818                    in (keywords_classification_table := SOME tab; tab) end)
   819 
   820 
   821 
   822     fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
   823         let
   824             val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
   825         in
   826             markup_text_attrs str "opentheory"
   827                               ([("thyname",thyname)] @
   828                                (if imports=[] then [] else
   829                                 [("parentnames", (space_implode ";" imports) ^ ";")]))
   830         end
   831 
   832     fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)
   833         let
   834             (* NB: PGIP only deals with single name bindings at the moment;
   835                potentially we could markup grouped definitions several times but
   836                that might suggest the wrong structure to the editor?
   837                Better alternative would be to put naming closer around text,
   838                but to do that we'd be much better off modifying the real parser
   839                instead of reconstructing it here. *)
   840 
   841             val plain_items = (* no names, unimportant names, or too difficult *)
   842                 ["defaultsort","arities","judgement","finalconsts",
   843                  "syntax", "nonterminals", "translations",
   844                  "global", "local", "hide",
   845                  "ML_setup", "setup", "method_setup",
   846                  "parse_ast_translation", "parse_translation", "print_translation",
   847                  "typed_print_translation", "print_ast_translation", "token_translation",
   848                  "oracle",
   849                  "declare"]
   850 
   851             val plain_item   = markup_text str "theoryitem"
   852             val comment_item = markup_text str "litcomment"
   853             val named_item   = named_item_elt toks str "theoryitem"
   854 
   855             val opt_overloaded = P.opt_keyword "overloaded";
   856 
   857             val thmnameP = (* see isar_syn.ML/theoremsP *)
   858                 let
   859                     val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
   860                     val theoremsP = P.opt_locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
   861                 in
   862                     theoremsP
   863                 end
   864         in
   865             (* TODO: ideally we would like to render terms properly, just as they are
   866                in output. This implies using PGML for symbols and variables/atoms.
   867                BUT it's rather tricky without having the correct concrete syntax to hand,
   868                and even if we did, we'd have to mess around here a whole lot more first
   869                to pick out the terms from the syntax. *)
   870 
   871             if (name mem plain_items) then plain_item
   872             else case name of
   873                      "text"      => comment_item
   874                    | "text_raw"  => comment_item
   875                    | "typedecl"  => named_item (P.type_args |-- P.name) "type"
   876                    | "types"     => named_item (P.type_args |-- P.name) "type"
   877                    | "classes"   => named_item P.name "class"
   878                    | "classrel"  => named_item P.name "class"
   879                    | "consts"    => named_item (P.const >> #1) "term"
   880                    | "axioms"    => named_item (P.spec_name >> (#1 o #1)) "theorem"
   881                    | "defs"      => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
   882                    | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
   883                    | "theorems"  => named_item thmnameP "thmset"
   884                    | "lemmas"    => named_item thmnameP "thmset"
   885                    | "oracle"    => named_item P.name "oracle"
   886                    | "locale"    => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
   887                    | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item)
   888         end
   889 
   890     fun xmls_of_thy_goal (name,toks,str) =
   891         let
   892             (* see isar_syn.ML/gen_theorem *)
   893          val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
   894          val general_statement =
   895             statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
   896 
   897             val gen_theoremP =
   898                 P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
   899                  Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
   900                                  general_statement >> (fn ((locale, a), (elems, concl)) =>
   901                                                          fst a) (* a : (bstring * Args.src list) *)
   902 
   903             val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
   904             (* TODO: add preference values for attributes
   905                val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
   906             *)
   907         in
   908             (thmnamed_item_elt toks str "opengoal" nameP "") @
   909             (empty "openblock")
   910         end
   911 
   912     fun xmls_of_qed (name,markup) =
   913         let val qedmarkup  =
   914                 (case name of
   915                      "sorry" => markup "postponegoal"
   916                    | "oops"  => markup "giveupgoal"
   917                    | "done"  => markup "closegoal"
   918                    | "by"    => markup "closegoal"  (* nested or toplevel *)
   919                    | "qed"   => markup "closegoal"  (* nested or toplevel *)
   920                    | "."     => markup "closegoal"  (* nested or toplevel *)
   921                    | ".."    => markup "closegoal"  (* nested or toplevel *)
   922                    | other => (* default to closegoal: may be wrong for extns *)
   923                                   (parse_warning
   924                                        ("Unrecognized qed command: " ^ quote other);
   925                                        markup "closegoal"))
   926         in qedmarkup @ (empty "closeblock") end
   927 
   928     fun xmls_of_kind kind (name,toks,str) =
   929     let val markup = markup_text str in
   930     case kind of
   931       "control"        => markup "badcmd"
   932     | "diag"           => markup "spuriouscmd"
   933     (* theory/files *)
   934     | "theory-begin"   => xmls_of_thy_begin (name,toks,str)
   935     | "theory-decl"    => xmls_of_thy_decl (name,toks,str)
   936     | "theory-heading" => markup "litcomment"
   937     | "theory-script"  => markup "theorystep"
   938     | "theory-end"     => markup "closetheory"
   939     (* proof control *)
   940     | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
   941     | "proof-heading"  => markup "litcomment"
   942     | "proof-goal"     => (markup "opengoal") @ (empty "openblock")  (* nested proof: have, show, ... *)
   943     | "proof-block"    => markup "proofstep" (* context-shift: proof, next; really "newgoal" *)
   944     | "proof-open"     => (empty "openblock") @ (markup "proofstep")
   945     | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
   946     | "proof-script"   => markup "proofstep"
   947     | "proof-chain"    => markup "proofstep"
   948     | "proof-decl"     => markup "proofstep"
   949     | "proof-asm"      => markup "proofstep"
   950     | "proof-asm-goal" => (markup "opengoal") @ (empty "openblock")  (* nested proof: obtain *)
   951     | "qed"            => xmls_of_qed (name,markup)
   952     | "qed-block"      => xmls_of_qed (name,markup)
   953     | "qed-global"     => xmls_of_qed (name,markup)
   954     | other => (* default for anything else is "spuriouscmd", ignored for undo. *)
   955       (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other);
   956        markup "spuriouscmd")
   957     end
   958 in
   959 
   960 fun xmls_of_transition (name,str,toks) =
   961    let
   962      val classification = Symtab.curried_lookup (get_keywords_classification_table ()) name
   963    in case classification of
   964           SOME k => (xmls_of_kind k (name,toks,str))
   965         | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
   966           (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
   967            markup_text str "spuriouscmd")
   968    end
   969 
   970 fun markup_toks [] _ = []
   971   | markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x
   972 
   973 fun markup_comment_whs [] = []
   974   | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
   975     let
   976         val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
   977     in
   978         if (prewhs <> []) then
   979             whitespace (implode (map OuterLex.unparse prewhs))
   980             :: (markup_comment_whs rest)
   981         else
   982             (markup_text (OuterLex.unparse t) "comment") @
   983             (markup_comment_whs ts)
   984     end
   985 
   986 fun xmls_pre_cmd [] = ([],[])
   987   | xmls_pre_cmd toks =
   988     let
   989         (* an extra token is needed to terminate the command *)
   990         val sync = OuterSyntax.scan "\\<^sync>";
   991         val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode
   992         val text_with_whs =
   993             ((spaceP || Scan.succeed "") --
   994              (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^)
   995              -- (spaceP || Scan.succeed "") >> op^
   996         val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync)
   997         (* NB: this collapses  litcomment,(litcomment|whitespace)* to a single litcomment *)
   998         val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1
   999         val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2
  1000     in
  1001         ((markup_comment_whs prewhs) @
  1002          (if (length rest2 = length rest1)  then []
  1003           else markup_text (implode
  1004                                 (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1))))
  1005                "litcomment") @
  1006          (markup_comment_whs postwhs),
  1007          Library.take (length rest3 - 1,rest3))
  1008     end
  1009 
  1010 fun xmls_of_impropers toks =
  1011     let
  1012         val (xmls,rest) = xmls_pre_cmd toks
  1013     in
  1014         xmls @ (markup_toks rest "unparseable")
  1015     end
  1016 
  1017 fun markup_unparseable str = markup_text str "unparseable"
  1018 
  1019 end
  1020 
  1021 
  1022 local
  1023     (* we have to weave together the whitespace/comments with proper tokens
  1024        to reconstruct the input. *)
  1025     (* TODO: see if duplicating isar_output/parse_thy can help here *)
  1026 
  1027     fun match_tokens ([],us,vs) = (rev vs,us)  (* used, unused *)
  1028       | match_tokens (t::ts,w::ws,vs) =
  1029         if (t = w) then match_tokens (ts,ws,w::vs)
  1030         else match_tokens (t::ts,ws,w::vs)
  1031       | match_tokens _ = error ("match_tokens: mismatched input parse")
  1032 in
  1033     fun xmls_of_str str =
  1034     let
  1035        (* parsing:   See outer_syntax.ML/toplevel_source *)
  1036        fun parse_loop ([],[],xmls) = xmls
  1037          | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
  1038          | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
  1039            let
  1040                (* first proper token after whitespace/litcomment/whitespace is command *)
  1041                val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
  1042                val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
  1043                                                      | _ => error("proof_general/parse_loop impossible")
  1044                val (utoks,itoks'') = match_tokens (toks,itoks',[])
  1045                (* FIXME: should take trailing [w/s+] semicolon too in utoks *)
  1046 
  1047                val str = implode (map OuterLex.unparse (cmdtok::utoks))
  1048 
  1049                val xmls_tr  = xmls_of_transition (nm,str,toks)
  1050            in
  1051                parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr)
  1052            end
  1053     in
  1054         (let val toks = OuterSyntax.scan str
  1055          in
  1056              parse_loop (OuterSyntax.read toks, toks, [])
  1057          end)
  1058            handle _ => markup_unparseable str
  1059     end
  1060 
  1061 
  1062 fun parsescript str attrs =
  1063     let
  1064         val _ = start_delay_msgs ()  (* accumulate error messages to put inside parseresult *)
  1065         val xmls = xmls_of_str str
  1066         val errs = end_delayed_msgs ()
  1067      in
  1068         issue_pgips [XML.element "parseresult" attrs (errs@xmls)]
  1069     end
  1070 end
  1071 
  1072 
  1073 
  1074 (**** PGIP:  Isabelle -> Interface ****)
  1075 
  1076 val isabelle_pgml_version_supported = "1.0";
  1077 val isabelle_pgip_version_supported = "2.0"
  1078 
  1079 (* TODO: would be cleaner to define a datatype here for the accepted elements,
  1080    and mapping functions to/from strings.  At the moment this list must
  1081    coincide with the strings in the function process_pgip_element. *)
  1082 val isabelle_acceptedpgipelems =
  1083     ["askpgip","askpgml","askprefs","getpref","setpref",
  1084      "proverinit","proverexit","startquiet","stopquiet",
  1085      "pgmlsymbolson", "pgmlsymbolsoff",
  1086      "dostep", "undostep", "redostep", "abortgoal", "forget", "restoregoal",
  1087      "askids", "showid", "askguise",
  1088      "parsescript",
  1089      "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
  1090      "doitem", "undoitem", "redoitem", "abortheory",
  1091      "retracttheory", "loadfile", "openfile", "closefile",
  1092      "abortfile", "changecwd", "systemcmd"];
  1093 
  1094 fun usespgip () =
  1095     issue_pgip
  1096         "usespgip"
  1097         [("version", isabelle_pgip_version_supported)]
  1098         (XML.element "acceptedpgipelems" []
  1099                      (map (fn s=>XML.element "pgipelem"
  1100                                              [] (* if threads: possibility to add async here *)
  1101                                              [s])
  1102                           isabelle_acceptedpgipelems))
  1103 
  1104 fun usespgml () =
  1105     issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)]
  1106 
  1107 fun hasprefs () =
  1108     List.app (fn (prefcat, prefs) =>
  1109             issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
  1110                  (map (fn (name, (descr, (ty, (default,_),_))) =>
  1111                        XML.element "haspref" [("name", name),
  1112                                               ("descr", descr),
  1113                                               ("default", default)]
  1114                        [ty]) prefs)]) (!preferences)
  1115 
  1116 fun allprefs () = Library.foldl (op @) ([], map snd (!preferences))
  1117 
  1118 fun setpref name value =
  1119     (case AList.lookup (op =) (allprefs ()) name of
  1120          NONE => warning ("Unknown pref: " ^ quote name)
  1121        | SOME (_, (_, _, set)) => set value);
  1122 
  1123 fun getpref name =
  1124     (case AList.lookup (op =) (allprefs ()) name of
  1125          NONE => warning ("Unknown pref: " ^ quote name)
  1126        | SOME (_, (_, (_,get), _)) =>
  1127            issue_pgip "prefval" [("name", name)] (get ()));
  1128 
  1129 
  1130 
  1131 (**** PGIP:  Interface -> Isabelle/Isar ****)
  1132 
  1133 exception PGIP of string;
  1134 exception PGIP_QUIT;
  1135 
  1136 
  1137 (* Sending commands to Isar *)
  1138 
  1139 fun isarcmd s =
  1140     s |> OuterSyntax.scan |> OuterSyntax.read
  1141       |> map (Toplevel.position (Position.name "PGIP message") o #3) |> Toplevel.>>>;
  1142 
  1143 fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts)
  1144   | xmltext [] = ""
  1145   | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
  1146 
  1147 fun isarscript xmls = isarcmd (xmltext xmls)   (* send a script command *)
  1148 
  1149 
  1150 (* load an arbitrary file (must be .thy or .ML) *)
  1151 
  1152 fun use_thy_or_ml_file file =
  1153     let
  1154         val (path,extn) = Path.split_ext (Path.unpack file)
  1155     in
  1156         case extn of
  1157             "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
  1158           | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
  1159           | "ML" => isarcmd ("use " ^ quote file)
  1160           | other => error ("Don't know how to read a file with extension " ^ other)
  1161     end
  1162 
  1163 
  1164 (* Proof control commands *)
  1165 
  1166 local
  1167   fun xmlattro attr attrs = AList.lookup (op =) attrs attr
  1168 
  1169   fun xmlattr attr attrs =
  1170       (case xmlattro attr attrs of
  1171            SOME value => value
  1172          | NONE => raise PGIP ("Missing attribute: " ^ attr))
  1173 
  1174   val thyname_attro = xmlattro "thyname"
  1175   val thyname_attr = xmlattr "thyname"
  1176   val objtype_attro = xmlattro "objtype"
  1177   val objtype_attr = xmlattr "objtype"
  1178   val name_attr = xmlattr "name"
  1179   val dirname_attr = xmlattr "dir"
  1180   fun comment x = "(* " ^ x ^ " *)"
  1181 
  1182   fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
  1183       case Url.unpack url of
  1184           (Url.File path) => File.platform_path path
  1185         | _ => error ("Cannot access non-local URL " ^ url)
  1186 
  1187   val fileurl_of = localfile_of_url o (xmlattr "url")
  1188 
  1189   val topthy = Toplevel.theory_of o Toplevel.get_state
  1190   val topthy_name = Context.theory_name o topthy
  1191 
  1192   val currently_open_file = ref (NONE : string option)
  1193 
  1194   (* Path management: we allow theory files to have dependencies
  1195      in their own directory, but when we change directory for a new
  1196      file we remove the path.  Leaving it there can cause confusion
  1197      with difference in batch mode.a  NB: PGIP does not assume
  1198      that the prover has a load path. *)
  1199   local
  1200       val current_working_dir = ref (NONE : string option)
  1201   in
  1202       fun changecwd dir =
  1203           (case (!current_working_dir) of
  1204                NONE => ()
  1205              | SOME dir => ThyLoad.del_path dir;
  1206            ThyLoad.add_path dir;
  1207            current_working_dir := SOME dir)
  1208   end
  1209 
  1210   val topnode = Toplevel.node_of o Toplevel.get_state
  1211   fun topproofpos () = (case topnode() of Toplevel.Proof ph => SOME(ProofHistory.position ph)
  1212                                         | _ => NONE) handle Toplevel.UNDEF => NONE
  1213 in
  1214 
  1215 fun process_pgip_element pgipxml = (case pgipxml of
  1216   (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
  1217 | (xml as (XML.Elem (elem, attrs, data))) =>
  1218   (case elem of
  1219        (* protocol config *)
  1220        "askpgip"        => (pgip_emacs_compatibility_flag:=false; (* PG>=3.6 or other PGIP interface *)
  1221                             usespgip (); send_pgip_config ())
  1222      | "askpgml"        => usespgml ()
  1223      (* proverconfig *)
  1224      | "askprefs"       => hasprefs ()
  1225      | "getpref"        => getpref (name_attr attrs)
  1226      | "setpref"        => setpref (name_attr attrs) (xmltext data)
  1227      (* provercontrol *)
  1228      | "proverinit"     => isar_restart ()
  1229      | "proverexit"     => isarcmd "quit"
  1230      | "startquiet"     => isarcmd "disable_pr"
  1231      | "stopquiet"      => isarcmd "enable_pr"
  1232      | "pgmlsymbolson"   => change print_mode (insert (op =) Symbol.xsymbolsN)
  1233      | "pgmlsymbolsoff"  => change print_mode (remove (op =) Symbol.xsymbolsN)
  1234      (* properproofcmd: proper commands which belong in script *)
  1235      (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
  1236      (* NB: Isar doesn't make lemma name of goal accessible during proof *)
  1237      | "opengoal"       => isarscript data
  1238      | "proofstep"      => isarscript data
  1239      | "closegoal"      => isarscript data
  1240      | "giveupgoal"     => isarscript data
  1241      | "postponegoal"   => isarscript data
  1242      | "comment"        => isarscript data  (* NB: should be ignored, but process anyway *)
  1243      | "whitespace"     => isarscript data  (* NB: should be ignored, but process anyway *)
  1244      | "litcomment"     => isarscript data
  1245      | "spuriouscmd"    => isarscript data
  1246      | "badcmd"         => isarscript data
  1247      (* improperproofcmd: improper commands which *do not* belong in script *)
  1248      | "dostep"         => isarscript data
  1249      | "undostep"       => isarcmd "undos_proof 1"
  1250      | "redostep"       => isarcmd "redo"
  1251      | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"
  1252      | "forget"         => error "Not implemented"
  1253      | "restoregoal"    => error "Not implemented"  (* could just treat as forget? *)
  1254      (* proofctxt: improper commands *)
  1255      | "askids"         => askids (thyname_attro attrs, objtype_attro attrs)
  1256      | "showid"         => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
  1257      | "askguise"       => send_informguise (!currently_open_file,
  1258                                              SOME (topthy_name()) handle Toplevel.UNDEF => NONE,
  1259                                              topproofpos())
  1260      | "parsescript"    => parsescript (xmltext data) attrs (* just pass back attrs unchanged *)
  1261      | "showproofstate" => isarcmd "pr"
  1262      | "showctxt"       => isarcmd "print_theory"   (* more useful than print_context *)
  1263      | "searchtheorems" => isarcmd ("thms_containing " ^ xmltext data)
  1264      | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ xmltext data)
  1265      | "viewdoc"        => isarcmd ("print_" ^ xmltext data) (* FIXME: isatool doc? *)
  1266      (* properfilecmd: proper theory-level script commands *)
  1267      (* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *)
  1268      | "opentheory"     => isarscript data
  1269      | "theoryitem"     => isarscript data
  1270      | "closetheory"    => let
  1271                               val thyname = topthy_name()
  1272                            in (isarscript data;
  1273                                writeln ("Theory " ^ quote thyname ^ " completed."))
  1274                            end
  1275      (* improperfilecmd: theory-level commands not in script *)
  1276      | "doitem"         => isarscript data
  1277      | "undoitem"       => isarcmd "ProofGeneral.undo"
  1278      | "redoitem"       => isarcmd "ProofGeneral.redo"
  1279      | "aborttheory"    => isarcmd ("init_toplevel")
  1280      | "retracttheory"  => isarcmd ("kill_thy " ^ quote (thyname_attr attrs))
  1281      | "loadfile"       => use_thy_or_ml_file (fileurl_of attrs)
  1282      | "openfile"       => (openfile_retract (fileurl_of attrs);
  1283                             currently_open_file := SOME (fileurl_of attrs))
  1284      | "closefile"      => (case !currently_open_file of
  1285                                 SOME f => (inform_file_processed f;
  1286                                            currently_open_file := NONE)
  1287                               | NONE => raise PGIP ("closefile when no file is open!"))
  1288      | "abortfile"      => (currently_open_file := NONE) (* perhaps error for no file open *)
  1289      | "changecwd"      => changecwd (dirname_attr attrs)
  1290      | "systemcmd"      => isarscript data
  1291      (* unofficial command for debugging *)
  1292      | "quitpgip" => raise PGIP_QUIT
  1293      | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
  1294 
  1295 fun process_pgip_tree xml =
  1296     (pgip_refid := NONE;
  1297      pgip_refseq := NONE;
  1298      (case xml of
  1299           XML.Elem ("pgip", attrs, pgips) =>
  1300           (let
  1301                val class = xmlattr "messageclass" attrs
  1302                val dest  = xmlattro "destid" attrs
  1303                val _ = (pgip_refid :=  xmlattro "id" attrs;
  1304                         pgip_refseq := xmlattro "seq" attrs)
  1305            in
  1306                (* We respond to broadcast messages to provers, or
  1307                   messages intended uniquely for us.  Silently ignore rest. *)
  1308                case dest of
  1309                    NONE => if (class = "pa") then
  1310                                (List.app process_pgip_element pgips; true)
  1311                            else false
  1312                  | SOME id => if (matching_pgip_id id) then
  1313                                   (List.app process_pgip_element pgips; true)
  1314                               else false
  1315            end)
  1316         | _ => raise PGIP "Invalid PGIP packet received")
  1317      handle (PGIP msg) =>
  1318             (error (msg ^ "\nPGIP error occured in XML text below:\n" ^
  1319                     (XML.string_of_tree xml))))
  1320 
  1321 val process_pgip = K () o process_pgip_tree o XML.tree_of_string
  1322 
  1323 end
  1324 
  1325 
  1326 (* PGIP loop: process PGIP input only *)
  1327 
  1328 local
  1329 
  1330 exception XML_PARSE
  1331 
  1332 fun loop ready src =
  1333     let
  1334         val _ = if ready then (issue_pgipe "ready" []) else ()
  1335         val pgipo = (Source.get_single src)
  1336                         handle e => raise XML_PARSE
  1337     in
  1338         case pgipo of
  1339              NONE  => ()
  1340            | SOME (pgip,src') =>
  1341              let
  1342                  val ready' = (process_pgip_tree pgip) handle e => (handler (e,SOME src'); true)
  1343              in
  1344                  loop ready' src'
  1345              end
  1346     end handle e => handler (e,SOME src)  (* i.e. error in ready/XML parse *)
  1347 
  1348 and handler (e,srco) =
  1349     case (e,srco) of
  1350         (XML_PARSE,SOME src) =>
  1351         panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *)
  1352       | (PGIP_QUIT,_) => ()
  1353       | (ERROR,SOME src) => loop true src (* message already given *)
  1354       | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src)
  1355       | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *)
  1356       | (e,SOME src) => (error (Toplevel.exn_message e); loop true src)
  1357       | (_,NONE) => ()
  1358 in
  1359   (* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *)
  1360 
  1361   val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
  1362 
  1363   val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
  1364 
  1365   fun pgip_toplevel x = loop true x
  1366 end
  1367 
  1368 
  1369 (* additional outer syntax for Isar *)
  1370 
  1371 local structure P = OuterParse and K = OuterKeyword in
  1372 
  1373 val undoP = (*undo without output*)
  1374   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
  1375     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
  1376 
  1377 val redoP = (*redo without output*)
  1378   OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
  1379     (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
  1380 
  1381 val context_thy_onlyP =
  1382   OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
  1383     (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
  1384 
  1385 val try_context_thy_onlyP =
  1386   OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
  1387     (P.name >> (Toplevel.no_timing oo
  1388       (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
  1389 
  1390 val restartP =
  1391   OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
  1392     (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
  1393 
  1394 val kill_proofP =
  1395   OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
  1396     (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
  1397 
  1398 val inform_file_processedP =
  1399   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
  1400     (P.name >> (fn file => Toplevel.no_timing o
  1401       Toplevel.keep (vacuous_inform_file_processed file) o
  1402       Toplevel.kill o
  1403       Toplevel.keep (proper_inform_file_processed file)));
  1404 
  1405 val inform_file_retractedP =
  1406   OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
  1407     (P.name >> (Toplevel.no_timing oo
  1408       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
  1409 
  1410 val process_pgipP =
  1411   OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
  1412     (P.text >> (Toplevel.no_timing oo
  1413       (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
  1414 
  1415 fun init_outer_syntax () = OuterSyntax.add_parsers
  1416  [undoP, redoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
  1417   inform_file_processedP, inform_file_retractedP, process_pgipP];
  1418 
  1419 end;
  1420 
  1421 
  1422 (* init *)
  1423 
  1424 val initialized = ref false;
  1425 
  1426 fun set_prompts true _ = ml_prompts "ML> " "ML# "
  1427   | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
  1428   | set_prompts false false = ml_prompts ("> " ^ special "372") ("- " ^ special "373");
  1429 
  1430 fun init_setup isar pgip =
  1431   (conditional (not (! initialized)) (fn () =>
  1432    (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
  1433     setup_xsymbols_output ();
  1434     setup_pgml_output ();
  1435     setup_messages ();
  1436     setup_state ();
  1437     setup_thy_loader ();
  1438     setup_present_hook ();
  1439     set initialized; ()));
  1440   sync_thy_loader ();
  1441   change print_mode (cons proof_generalN o remove (op =) proof_generalN);
  1442   if pgip then
  1443       (init_pgip_session_id();
  1444        change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN]))
  1445   else
  1446     pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
  1447   set quick_and_dirty;
  1448   ThmDeps.enable ();
  1449   set_prompts isar pgip;
  1450   pgip_active := pgip);
  1451 
  1452 fun init isar =
  1453  (init_setup isar false;
  1454   if isar then Isar.sync_main () else isa_restart ());
  1455 
  1456 fun init_pgip false = panic "PGIP not supported for Isabelle/classic mode."
  1457   | init_pgip true = (init_setup true true; pgip_toplevel tty_src);
  1458 
  1459 
  1460 
  1461 (** generate elisp file for keyword classification **)
  1462 
  1463 local
  1464 
  1465 val regexp_meta = explode ".*+?[]^$";
  1466 val regexp_quote =
  1467   implode o map (fn c => if c mem_string regexp_meta then "\\\\" ^ c else c) o explode;
  1468 
  1469 fun defconst name strs =
  1470   "\n(defconst isar-keywords-" ^ name ^
  1471   "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
  1472 
  1473 fun make_elisp_commands commands kind = defconst kind
  1474   (commands |> List.mapPartial (fn (c, _, k, _) => if k = kind then SOME c else NONE));
  1475 
  1476 fun make_elisp_syntax (keywords, commands) =
  1477   ";;\n\
  1478   \;; Keyword classification tables for Isabelle/Isar.\n\
  1479   \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
  1480   \;;\n\
  1481   \;; $" ^ "Id$\n\
  1482   \;;\n" ^
  1483   defconst "major" (map #1 commands) ^
  1484   defconst "minor" (List.filter Syntax.is_identifier keywords) ^
  1485   implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
  1486   "\n(provide 'isar-keywords)\n";
  1487 
  1488 in
  1489 
  1490 fun write_keywords s =
  1491  (init_outer_syntax ();
  1492   File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
  1493     (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
  1494 
  1495 end;
  1496 
  1497 end;