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