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