src/Pure/proof_general.ML
author wenzelm
Wed Aug 09 00:12:35 2006 +0200 (2006-08-09)
changeset 20364 f7e440f2eb2f
parent 20299 5330f710b960
child 20642 cfe2b0803a51
permissions -rw-r--r--
int_option: signed_string_of_int;
     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 path = url_attr ("file:///" ^ path);
   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 path))]
   318   else
   319     emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
   320 
   321 fun tell_file_retracted path =
   322   if pgip() then
   323     issue_pgipe "informfileretracted"
   324       [localfile_url_attr  (XML.text (File.platform_path path))]
   325   else
   326     emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
   327 
   328 
   329 (* theory / proof state output *)
   330 
   331 local
   332 
   333 fun tmp_markers f =
   334   setmp Display.current_goals_markers (special "366", special "367", "") f ();
   335 
   336 fun statedisplay prts =
   337   issue_pgip "proofstate" []
   338     (XML.element "pgml" []
   339       [XML.element "statedisplay" [] [Pretty.output (Pretty.chunks prts)]]);
   340 
   341 fun print_current_goals n m st =
   342   if pgml () then statedisplay (Display.pretty_current_goals n m st)
   343   else tmp_markers (fn () => Display.print_current_goals_default n m st);
   344 
   345 fun print_state b st =
   346   if pgml () then statedisplay (Toplevel.pretty_state b st)
   347   else tmp_markers (fn () => Toplevel.print_state_default b st);
   348 
   349 in
   350 
   351 fun setup_state () =
   352   (Display.print_current_goals_fn := print_current_goals;
   353    Toplevel.print_state_fn := print_state;
   354    (* FIXME: check next octal char won't appear in pgip? *)
   355    Toplevel.prompt_state_fn := (fn s => suffix (special "372")
   356      (Toplevel.prompt_state_default s)));
   357 
   358 end;
   359 
   360 end;
   361 
   362 
   363 (* misc commands for ProofGeneral/isa *)
   364 
   365 fun thms_containing ss =
   366   FindTheorems.print_theorems (ProofContext.init (the_context ())) NONE NONE
   367     (map (fn s => (true, FindTheorems.Pattern s)) ss);
   368 
   369 val welcome = priority o Session.welcome;
   370 val help = welcome;
   371 val show_context = Context.the_context;
   372 
   373 fun kill_goal () = (OldGoals.reset_goals (); tell_clear_goals ());
   374 
   375 fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
   376 
   377 fun repeat_undo 0 = ()
   378   | repeat_undo 1 = undo ()
   379   | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
   380 
   381 
   382 (* theory loader actions *)
   383 
   384 local
   385 
   386 fun add_master_files name files =
   387   let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
   388   in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
   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 (add_master_files name (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 
   627 (* Configuration: GUI config, proverinfo messages *)
   628 
   629 
   630 fun orenv v d = case (getenv v) of "" => d  | s => s
   631 
   632 local
   633     fun config_file()  = orenv "ISABELLE_PGIPCONFIG" "~~/lib/ProofGeneral/pgip_isar.xml"
   634     fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" "http://isabelle.in.tum.de/"
   635 in
   636 fun send_pgip_config () =
   637     let
   638         val path = Path.unpack (config_file())
   639         val exists = File.exists path
   640         val proverinfo =
   641             XML.element "proverinfo"
   642               [("name",     	 "Isabelle"), 
   643 	       ("version",  	 version),
   644 	       ("instance", 	 Session.name()), 
   645 	       ("descr",	 "The Isabelle/Isar theorem prover"),
   646 	       ("url",      	 isabelle_www()),   
   647 	       ("filenameextns", ".thy;")]
   648             []
   649     in
   650         if exists then
   651             (issue_pgips [proverinfo]; issue_pgips [File.read path])
   652         else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
   653     end;
   654 end
   655 
   656 
   657 (* Reveal some information about prover state *)
   658 fun send_informguise (openfile, opentheory, openproofpos) =
   659     let val guisefile =
   660             case openfile of SOME f => [XML.element "guisefile"
   661                                                     [("url",Url.pack (Url.File (Path.unpack f)))] []]
   662                            | _ => []
   663         val guisetheory =
   664             case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
   665                              | _ => []
   666         val guiseproof =
   667             case openproofpos of SOME i => [XML.element "guiseproof" [("proofpos", string_of_int i)] []]
   668                                | _ => []
   669     in
   670         issue_pgips [XML.element "informguise" [] (guisefile @ guisetheory @ guiseproof)]
   671     end
   672 
   673 
   674 (* PGIP identifier tables (prover objects). [incomplete] *)
   675 
   676 local
   677     val objtype_thy  = "theory"
   678     val objtype_thm  = "theorem"
   679     val objtype_term = "term"
   680     val objtype_type = "type"
   681 
   682     fun xml_idtable ty ctx ids =
   683         let
   684             fun ctx_attr (SOME c)= [("context", c)]
   685               | ctx_attr NONE    = []
   686             fun xmlid x = XML.element "identifier" [] [XML.text x];
   687         in
   688             XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
   689                                   (map xmlid ids)
   690         end
   691 in
   692 
   693 fun setids t = issue_pgip "setids" [] t
   694 fun addids t = issue_pgip "addids" [] t
   695 fun delids t = issue_pgip "delids" [] t
   696 
   697 fun delallids ty = setids (xml_idtable ty NONE [])
   698 
   699 fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
   700 fun clear_thy_idtable () = delallids objtype_thy
   701 
   702 fun send_thm_idtable ctx thy =
   703     addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy)));
   704 
   705 fun clear_thm_idtable () = delallids objtype_thm
   706 
   707 (* fun send_type_idtable thy = TODO, it's a bit low-level messy
   708    & maybe not so useful anyway *)
   709 
   710 end
   711 
   712 (* Response to interface queries about known objects *)
   713 
   714 local
   715  val topthy = Toplevel.theory_of o Toplevel.get_state
   716  fun pthm thy name = print_thm (get_thm thy (Name name))
   717 
   718  fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
   719 in
   720 (* FIXME: add askids for "file" here, which returns single theory with same name *)
   721 fun askids (NONE, SOME "theory")  = send_thy_idtable NONE (ThyInfo.names())
   722   | askids (NONE, NONE) =  send_thy_idtable NONE (ThyInfo.names())
   723                            (* only theories known in top context *)
   724   | askids (SOME thy, SOME "theory") = send_thy_idtable (SOME thy) (ThyInfo.get_preds thy)
   725   | askids (SOME thy, SOME "theorem") = send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)
   726   | askids (SOME thy, NONE) = (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy);
   727                                send_thm_idtable (SOME thy) (ThyInfo.get_theory thy))
   728   | askids (_, SOME ot) = error ("No objects of type "^(quote ot)^" are available here.")
   729 
   730 fun showid (_,        "theory", n) =
   731     with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
   732   | showid (SOME thy, "theorem", t) =
   733     with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
   734   | showid (NONE,     "theorem", t) =
   735     with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t)
   736   | showid (_, ot, _) = error ("Cannot show objects of type "^ot)
   737 
   738 end
   739 
   740 
   741 (** Parsing proof scripts without execution **)
   742 
   743 (* Notes.
   744    This is quite tricky, because 1) we need to put back whitespace which
   745    was removed during parsing so we can provide markup around commands;
   746    2) parsing is intertwined with execution in Isar so we have to repeat
   747    the parsing to extract interesting parts of commands.  The trace of
   748    tokens parsed which is now recorded in each transition (added by
   749    Markus June '04) helps do this, but the mechanism is still a bad mess.
   750 
   751    If we had proper parse trees it would be easy, although having a
   752    fixed type of trees might be tricky with Isar's extensible parser.
   753 
   754    Probably the best solution is to produce the meta-information at
   755    the same time as the parse, for each command, e.g. by recording a
   756    list of (name,objtype) pairs which record the bindings created by
   757    a command.  This would require changing the interfaces in
   758    outer_syntax.ML (or providing new ones),
   759 
   760     datatype metainfo = Binding of string * string  (* name, objtype *)
   761 
   762     val command_withmetainfo: string -> string -> string ->
   763       (token list ->
   764        ((Toplevel.transition -> Toplevel.transition) * metainfo list) *
   765        token list) -> parser
   766 
   767    We'd also like to render terms as they appear in output, but this
   768    will be difficult because inner syntax is extensible and we don't
   769    have the correct syntax to hand when just doing outer parsing
   770    without execution.  A reasonable approximation could
   771    perhaps be obtained by using the syntax of the current context.
   772    However, this would mean more mess trying to pick out terms,
   773    so at this stage a more serious change to the Isar functions
   774    seems necessary.
   775 *)
   776 
   777 local
   778     fun markup_text str elt = [XML.element elt [] [XML.text str]]
   779     fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
   780     fun empty elt = [XML.element elt [] []]
   781 
   782     fun whitespace str = XML.element "whitespace" [] [XML.text str]
   783 
   784     (* an extra token is needed to terminate the command *)
   785     val sync = OuterSyntax.scan "\\<^sync>";
   786 
   787     fun named_item_elt_with nameattr toks str elt nameP objtyp =
   788         let
   789             val name = (fst (nameP (toks@sync)))
   790                         handle _ => (error ("Error occurred in name parser for " ^ elt ^
   791                                             "(objtype: " ^ objtyp ^ ")");
   792                                      "")
   793 
   794         in
   795             [XML.element elt
   796                          ((if name="" then [] else [(nameattr, name)])@
   797                           (if objtyp="" then [] else [("objtype", objtyp)]))
   798                          ([XML.text str])]
   799         end
   800 
   801     val named_item_elt = named_item_elt_with "name"
   802     val thmnamed_item_elt = named_item_elt_with "thmname"
   803 
   804     fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg)
   805 
   806     (* FIXME: allow dynamic extensions to language here: we need a hook in
   807        outer_syntax.ML to reset this table. *)
   808 
   809     val keywords_classification_table = ref (NONE: string Symtab.table option)
   810 
   811     fun get_keywords_classification_table () =
   812         case (!keywords_classification_table) of
   813           SOME t => t
   814         | NONE => (let
   815                      val tab = fold (fn (c, _, k, _) => Symtab.update (c, k))
   816                                     (OuterSyntax.dest_parsers ()) Symtab.empty;
   817                    in (keywords_classification_table := SOME tab; tab) end)
   818 
   819 
   820 
   821     fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
   822         let
   823             val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
   824         in
   825             markup_text_attrs str "opentheory"
   826                               ([("thyname",thyname)] @
   827                                (if imports=[] then [] else
   828                                 [("parentnames", (space_implode ";" imports) ^ ";")]))
   829         end
   830 
   831     fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)
   832         let
   833             (* NB: PGIP only deals with single name bindings at the moment;
   834                potentially we could markup grouped definitions several times but
   835                that might suggest the wrong structure to the editor?
   836                Better alternative would be to put naming closer around text,
   837                but to do that we'd be much better off modifying the real parser
   838                instead of reconstructing it here. *)
   839 
   840             val plain_items = (* no names, unimportant names, or too difficult *)
   841                 ["defaultsort","arities","judgement","finalconsts",
   842                  "syntax", "nonterminals", "translations",
   843                  "global", "local", "hide",
   844                  "ML_setup", "setup", "method_setup",
   845                  "parse_ast_translation", "parse_translation", "print_translation",
   846                  "typed_print_translation", "print_ast_translation", "token_translation",
   847                  "oracle",
   848                  "declare"]
   849 
   850             val plain_item   = markup_text str "theoryitem"
   851             val comment_item = markup_text str "litcomment"
   852             val named_item   = named_item_elt toks str "theoryitem"
   853 
   854             val opt_overloaded = P.opt_keyword "overloaded";
   855 
   856             val thmnameP = (* see isar_syn.ML/theoremsP *)
   857                 let
   858                     val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
   859                     val theoremsP = P.opt_locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
   860                 in
   861                     theoremsP
   862                 end
   863         in
   864             (* TODO: ideally we would like to render terms properly, just as they are
   865                in output. This implies using PGML for symbols and variables/atoms.
   866                BUT it's rather tricky without having the correct concrete syntax to hand,
   867                and even if we did, we'd have to mess around here a whole lot more first
   868                to pick out the terms from the syntax. *)
   869 
   870             if (name mem plain_items) then plain_item
   871             else case name of
   872                      "text"      => comment_item
   873                    | "text_raw"  => comment_item
   874                    | "typedecl"  => named_item (P.type_args |-- P.name) "type"
   875                    | "types"     => named_item (P.type_args |-- P.name) "type"
   876                    | "classes"   => named_item P.name "class"
   877                    | "classrel"  => named_item P.name "class"
   878                    | "consts"    => named_item (P.const >> #1) "term"
   879                    | "axioms"    => named_item (P.spec_name >> (#1 o #1)) "theorem"
   880                    | "defs"      => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
   881                    | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
   882                    | "theorems"  => named_item thmnameP "thmset"
   883                    | "lemmas"    => named_item thmnameP "thmset"
   884                    | "oracle"    => named_item P.name "oracle"
   885                    | "locale"    => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
   886                    | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item)
   887         end
   888 
   889     fun xmls_of_thy_goal (name,toks,str) =
   890         let
   891             (* see isar_syn.ML/gen_theorem *)
   892          val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
   893          val general_statement =
   894             statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
   895 
   896             val gen_theoremP =
   897                 P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
   898                  Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
   899                                  general_statement >> (fn ((locale, a), (elems, concl)) =>
   900                                                          fst a) (* a : (bstring * Args.src list) *)
   901 
   902             val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
   903             (* TODO: add preference values for attributes
   904                val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
   905             *)
   906         in
   907             (thmnamed_item_elt toks str "opengoal" nameP "") @
   908             (empty "openblock")
   909         end
   910 
   911     fun xmls_of_qed (name,markup) =
   912         let val qedmarkup  =
   913                 (case name of
   914                      "sorry" => markup "postponegoal"
   915                    | "oops"  => markup "giveupgoal"
   916                    | "done"  => markup "closegoal"
   917                    | "by"    => markup "closegoal"  (* nested or toplevel *)
   918                    | "qed"   => markup "closegoal"  (* nested or toplevel *)
   919                    | "."     => markup "closegoal"  (* nested or toplevel *)
   920                    | ".."    => markup "closegoal"  (* nested or toplevel *)
   921                    | other => (* default to closegoal: may be wrong for extns *)
   922                                   (parse_warning
   923                                        ("Unrecognized qed command: " ^ quote other);
   924                                        markup "closegoal"))
   925         in qedmarkup @ (empty "closeblock") end
   926 
   927     fun xmls_of_kind kind (name,toks,str) =
   928     let val markup = markup_text str in
   929     case kind of
   930       "control"        => markup "badcmd"
   931     | "diag"           => markup "spuriouscmd"
   932     (* theory/files *)
   933     | "theory-begin"   => xmls_of_thy_begin (name,toks,str)
   934     | "theory-decl"    => xmls_of_thy_decl (name,toks,str)
   935     | "theory-heading" => markup "litcomment"
   936     | "theory-script"  => markup "theorystep"
   937     | "theory-end"     => markup "closetheory"
   938     (* proof control *)
   939     | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
   940     | "proof-heading"  => markup "litcomment"
   941     | "proof-goal"     => (markup "opengoal") @ (empty "openblock")  (* nested proof: have, show, ... *)
   942     | "proof-block"    => markup "proofstep" (* context-shift: proof, next; really "newgoal" *)
   943     | "proof-open"     => (empty "openblock") @ (markup "proofstep")
   944     | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
   945     | "proof-script"   => markup "proofstep"
   946     | "proof-chain"    => markup "proofstep"
   947     | "proof-decl"     => markup "proofstep"
   948     | "proof-asm"      => markup "proofstep"
   949     | "proof-asm-goal" => (markup "opengoal") @ (empty "openblock")  (* nested proof: obtain *)
   950     | "qed"            => xmls_of_qed (name,markup)
   951     | "qed-block"      => xmls_of_qed (name,markup)
   952     | "qed-global"     => xmls_of_qed (name,markup)
   953     | other => (* default for anything else is "spuriouscmd", ignored for undo. *)
   954       (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other);
   955        markup "spuriouscmd")
   956     end
   957 in
   958 
   959 fun xmls_of_transition (name,str,toks) =
   960    let
   961      val classification = Symtab.lookup (get_keywords_classification_table ()) name
   962    in case classification of
   963           SOME k => (xmls_of_kind k (name,toks,str))
   964         | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
   965           (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
   966            markup_text str "spuriouscmd")
   967    end
   968 
   969 fun markup_toks [] _ = []
   970   | markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x
   971 
   972 fun markup_comment_whs [] = []
   973   | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
   974     let
   975         val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
   976     in
   977         if (prewhs <> []) then
   978             whitespace (implode (map OuterLex.unparse prewhs))
   979             :: (markup_comment_whs rest)
   980         else
   981             (markup_text (OuterLex.unparse t) "comment") @
   982             (markup_comment_whs ts)
   983     end
   984 
   985 fun xmls_pre_cmd [] = ([],[])
   986   | xmls_pre_cmd toks =
   987     let
   988         (* an extra token is needed to terminate the command *)
   989         val sync = OuterSyntax.scan "\\<^sync>";
   990         val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode
   991         val text_with_whs =
   992             ((spaceP || Scan.succeed "") --
   993              (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^)
   994              -- (spaceP || Scan.succeed "") >> op^
   995         val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync)
   996         (* NB: this collapses  litcomment,(litcomment|whitespace)* to a single litcomment *)
   997         val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1
   998         val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2
   999     in
  1000         ((markup_comment_whs prewhs) @
  1001          (if (length rest2 = length rest1)  then []
  1002           else markup_text (implode
  1003                                 (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1))))
  1004                "litcomment") @
  1005          (markup_comment_whs postwhs),
  1006          Library.take (length rest3 - 1,rest3))
  1007     end
  1008 
  1009 fun xmls_of_impropers toks =
  1010     let
  1011         val (xmls,rest) = xmls_pre_cmd toks
  1012     in
  1013         xmls @ (markup_toks rest "unparseable")
  1014     end
  1015 
  1016 fun markup_unparseable str = markup_text str "unparseable"
  1017 
  1018 end
  1019 
  1020 
  1021 local
  1022     (* we have to weave together the whitespace/comments with proper tokens
  1023        to reconstruct the input. *)
  1024     (* TODO: see if duplicating isar_output/parse_thy can help here *)
  1025 
  1026     fun match_tokens ([],us,vs) = (rev vs,us)  (* used, unused *)
  1027       | match_tokens (t::ts,w::ws,vs) =
  1028         if (t = w) then match_tokens (ts,ws,w::vs)
  1029         else match_tokens (t::ts,ws,w::vs)
  1030       | match_tokens _ = error ("match_tokens: mismatched input parse")
  1031 in
  1032     fun xmls_of_str str =
  1033     let
  1034        (* parsing:   See outer_syntax.ML/toplevel_source *)
  1035        fun parse_loop ([],[],xmls) = xmls
  1036          | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
  1037          | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
  1038            let
  1039                (* first proper token after whitespace/litcomment/whitespace is command *)
  1040                val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
  1041                val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
  1042                                                      | _ => error("proof_general/parse_loop impossible")
  1043                val (utoks,itoks'') = match_tokens (toks,itoks',[])
  1044                (* FIXME: should take trailing [w/s+] semicolon too in utoks *)
  1045 
  1046                val str = implode (map OuterLex.unparse (cmdtok::utoks))
  1047 
  1048                val xmls_tr  = xmls_of_transition (nm,str,toks)
  1049            in
  1050                parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr)
  1051            end
  1052     in
  1053         (let val toks = OuterSyntax.scan str
  1054          in
  1055              parse_loop (OuterSyntax.read toks, toks, [])
  1056          end)
  1057            handle _ => markup_unparseable str
  1058     end
  1059 
  1060 
  1061 fun parsescript str attrs =
  1062     let
  1063         val _ = start_delay_msgs ()  (* accumulate error messages to put inside parseresult *)
  1064         val xmls = xmls_of_str str
  1065         val errs = end_delayed_msgs ()
  1066      in
  1067         issue_pgips [XML.element "parseresult" attrs (errs@xmls)]
  1068     end
  1069 end
  1070 
  1071 
  1072 
  1073 (**** PGIP:  Isabelle -> Interface ****)
  1074 
  1075 val isabelle_pgml_version_supported = "1.0";
  1076 val isabelle_pgip_version_supported = "2.0"
  1077 
  1078 (* TODO: would be cleaner to define a datatype here for the accepted elements,
  1079    and mapping functions to/from strings.  At the moment this list must
  1080    coincide with the strings in the function process_pgip_element. *)
  1081 val isabelle_acceptedpgipelems =
  1082     ["askpgip","askpgml","askprefs","getpref","setpref",
  1083      "proverinit","proverexit","startquiet","stopquiet",
  1084      "pgmlsymbolson", "pgmlsymbolsoff",
  1085      "dostep", "undostep", "redostep", "abortgoal", "forget", "restoregoal",
  1086      "askids", "showid", "askguise",
  1087      "parsescript",
  1088      "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
  1089      "doitem", "undoitem", "redoitem", "abortheory",
  1090      "retracttheory", "loadfile", "openfile", "closefile",
  1091      "abortfile", "changecwd", "systemcmd"];
  1092 
  1093 fun usespgip () =
  1094     issue_pgip
  1095         "usespgip"
  1096         [("version", isabelle_pgip_version_supported)]
  1097         (XML.element "acceptedpgipelems" []
  1098                      (map (fn s=>XML.element "pgipelem"
  1099                                              [] (* if threads: possibility to add async here *)
  1100                                              [s])
  1101                           isabelle_acceptedpgipelems))
  1102 
  1103 fun usespgml () =
  1104     issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)]
  1105 
  1106 fun hasprefs () =
  1107     List.app (fn (prefcat, prefs) =>
  1108             issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
  1109                  (map (fn (name, (descr, (ty, (default,_),_))) =>
  1110                        XML.element "haspref" [("name", name),
  1111                                               ("descr", descr),
  1112                                               ("default", default)]
  1113                        [ty]) prefs)]) (!preferences)
  1114 
  1115 fun allprefs () = maps snd (!preferences)
  1116 
  1117 fun setpref name value =
  1118     (case AList.lookup (op =) (allprefs ()) name of
  1119          NONE => warning ("Unknown pref: " ^ quote name)
  1120        | SOME (_, (_, _, set)) => set value);
  1121 
  1122 fun getpref name =
  1123     (case AList.lookup (op =) (allprefs ()) name of
  1124          NONE => warning ("Unknown pref: " ^ quote name)
  1125        | SOME (_, (_, (_,get), _)) =>
  1126            issue_pgip "prefval" [("name", name)] (get ()));
  1127 
  1128 
  1129 
  1130 (**** PGIP:  Interface -> Isabelle/Isar ****)
  1131 
  1132 exception PGIP of string;
  1133 exception PGIP_QUIT;
  1134 
  1135 
  1136 (* Sending commands to Isar *)
  1137 
  1138 fun isarcmd s =
  1139     s |> OuterSyntax.scan |> OuterSyntax.read
  1140       |> map (Toplevel.position (Position.name "PGIP message") o #3) |> Toplevel.>>>;
  1141 
  1142 fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts)
  1143   | xmltext [] = ""
  1144   | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
  1145 
  1146 fun isarscript xmls = isarcmd (xmltext xmls)   (* send a script command *)
  1147 
  1148 
  1149 (* load an arbitrary file (must be .thy or .ML) *)
  1150 
  1151 fun use_thy_or_ml_file file =
  1152     let
  1153         val (path,extn) = Path.split_ext (Path.unpack file)
  1154     in
  1155         case extn of
  1156             "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
  1157           | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
  1158           | "ML" => isarcmd ("use " ^ quote file)
  1159           | other => error ("Don't know how to read a file with extension " ^ other)
  1160     end
  1161 
  1162 
  1163 (* Proof control commands *)
  1164 
  1165 local
  1166   fun xmlattro attr attrs = AList.lookup (op =) attrs attr
  1167 
  1168   fun xmlattr attr attrs =
  1169       (case xmlattro attr attrs of
  1170            SOME value => value
  1171          | NONE => raise PGIP ("Missing attribute: " ^ attr))
  1172 
  1173   val thyname_attro = xmlattro "thyname"
  1174   val thyname_attr = xmlattr "thyname"
  1175   val objtype_attro = xmlattro "objtype"
  1176   val objtype_attr = xmlattr "objtype"
  1177   val name_attr = xmlattr "name"
  1178   val dirname_attr = xmlattr "dir"
  1179   fun comment x = "(* " ^ x ^ " *)"
  1180 
  1181   fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
  1182       case Url.unpack url of
  1183           (Url.File path) => File.platform_path path
  1184         | _ => error ("Cannot access non-local URL " ^ url)
  1185 
  1186   val fileurl_of = localfile_of_url o (xmlattr "url")
  1187 
  1188   val topthy = Toplevel.theory_of o Toplevel.get_state
  1189   val topthy_name = Context.theory_name o topthy
  1190 
  1191   val currently_open_file = ref (NONE : string option)
  1192 
  1193   (* Path management: we allow theory files to have dependencies
  1194      in their own directory, but when we change directory for a new
  1195      file we remove the path.  Leaving it there can cause confusion
  1196      with difference in batch mode.a  NB: PGIP does not assume
  1197      that the prover has a load path. *)
  1198   local
  1199       val current_working_dir = ref (NONE : string option)
  1200   in
  1201       fun changecwd dir =
  1202           (case (!current_working_dir) of
  1203                NONE => ()
  1204              | SOME dir => ThyLoad.del_path dir;
  1205            ThyLoad.add_path dir;
  1206            current_working_dir := SOME dir)
  1207   end
  1208 
  1209   fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
  1210 in
  1211 
  1212 fun process_pgip_element pgipxml = (case pgipxml of
  1213   (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
  1214 | (xml as (XML.Elem (elem, attrs, data))) =>
  1215   (case elem of
  1216        (* protocol config *)
  1217        "askpgip"        => (pgip_emacs_compatibility_flag:=false; (* PG>=3.6 or other PGIP interface *)
  1218                             usespgip (); send_pgip_config ())
  1219      | "askpgml"        => usespgml ()
  1220      (* proverconfig *)
  1221      | "askprefs"       => hasprefs ()
  1222      | "getpref"        => getpref (name_attr attrs)
  1223      | "setpref"        => setpref (name_attr attrs) (xmltext data)
  1224      (* provercontrol *)
  1225      | "proverinit"     => isar_restart ()
  1226      | "proverexit"     => isarcmd "quit"
  1227      | "startquiet"     => isarcmd "disable_pr"
  1228      | "stopquiet"      => isarcmd "enable_pr"
  1229      | "pgmlsymbolson"   => change print_mode (fn mode =>
  1230           remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN])
  1231      | "pgmlsymbolsoff"  => change print_mode (remove (op =) Symbol.xsymbolsN)
  1232      (* properproofcmd: proper commands which belong in script *)
  1233      (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
  1234      (* NB: Isar doesn't make lemma name of goal accessible during proof *)
  1235      | "opengoal"       => isarscript data
  1236      | "proofstep"      => isarscript data
  1237      | "closegoal"      => isarscript data
  1238      | "giveupgoal"     => isarscript data
  1239      | "postponegoal"   => isarscript data
  1240      | "comment"        => isarscript data  (* NB: should be ignored, but process anyway *)
  1241      | "whitespace"     => isarscript data  (* NB: should be ignored, but process anyway *)
  1242      | "litcomment"     => isarscript data
  1243      | "spuriouscmd"    => isarscript data
  1244      | "badcmd"         => isarscript data
  1245      (* improperproofcmd: improper commands which *do not* belong in script *)
  1246      | "dostep"         => isarscript data
  1247      | "undostep"       => isarcmd "undos_proof 1"
  1248      | "redostep"       => isarcmd "redo"
  1249      | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"
  1250      | "forget"         => error "Not implemented"
  1251      | "restoregoal"    => error "Not implemented"  (* could just treat as forget? *)
  1252      (* proofctxt: improper commands *)
  1253      | "askids"         => askids (thyname_attro attrs, objtype_attro attrs)
  1254      | "showid"         => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
  1255      | "askguise"       => send_informguise (!currently_open_file,
  1256                                              SOME (topthy_name()) handle Toplevel.UNDEF => NONE,
  1257                                              topproofpos())
  1258      | "parsescript"    => parsescript (xmltext data) attrs (* just pass back attrs unchanged *)
  1259      | "showproofstate" => isarcmd "pr"
  1260      | "showctxt"       => isarcmd "print_theory"   (* more useful than print_context *)
  1261      | "searchtheorems" => isarcmd ("thms_containing " ^ xmltext data)
  1262      | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ xmltext data)
  1263      | "viewdoc"        => isarcmd ("print_" ^ xmltext data) (* FIXME: isatool doc? *)
  1264      (* properfilecmd: proper theory-level script commands *)
  1265      (* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *)
  1266      | "opentheory"     => isarscript data
  1267      | "theoryitem"     => isarscript data
  1268      | "closetheory"    => let
  1269                               val thyname = topthy_name()
  1270                            in (isarscript data;
  1271                                writeln ("Theory " ^ quote thyname ^ " completed."))
  1272                            end
  1273      (* improperfilecmd: theory-level commands not in script *)
  1274      | "doitem"         => isarscript data
  1275      | "undoitem"       => isarcmd "ProofGeneral.undo"
  1276      | "redoitem"       => isarcmd "ProofGeneral.redo"
  1277      | "aborttheory"    => isarcmd ("init_toplevel")
  1278      | "retracttheory"  => isarcmd ("kill_thy " ^ quote (thyname_attr attrs))
  1279      | "loadfile"       => use_thy_or_ml_file (fileurl_of attrs)
  1280      | "openfile"       => (openfile_retract (fileurl_of attrs);
  1281                             currently_open_file := SOME (fileurl_of attrs))
  1282      | "closefile"      => (case !currently_open_file of
  1283                                 SOME f => (inform_file_processed f;
  1284                                            currently_open_file := NONE)
  1285                               | NONE => raise PGIP ("closefile when no file is open!"))
  1286      | "abortfile"      => (currently_open_file := NONE) (* perhaps error for no file open *)
  1287      | "changecwd"      => changecwd (dirname_attr attrs)
  1288      | "systemcmd"      => isarscript data
  1289      (* unofficial command for debugging *)
  1290      | "quitpgip" => raise PGIP_QUIT
  1291      | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
  1292 
  1293 fun process_pgip_tree xml =
  1294     (pgip_refid := NONE;
  1295      pgip_refseq := NONE;
  1296      (case xml of
  1297           XML.Elem ("pgip", attrs, pgips) =>
  1298           (let
  1299                val class = xmlattr "class" attrs
  1300                val dest  = xmlattro "destid" attrs
  1301                val _ = (pgip_refid :=  xmlattro "id" attrs;
  1302                         pgip_refseq := xmlattro "seq" attrs)
  1303            in
  1304                (* We respond to broadcast messages to provers, or
  1305                   messages intended uniquely for us.  Silently ignore rest. *)
  1306                case dest of
  1307                    NONE => if (class = "pa") then
  1308                                (List.app process_pgip_element pgips; true)
  1309                            else false
  1310                  | SOME id => if (matching_pgip_id id) then
  1311                                   (List.app process_pgip_element pgips; true)
  1312                               else false
  1313            end)
  1314         | _ => raise PGIP "Invalid PGIP packet received")
  1315      handle PGIP msg =>
  1316             error (msg ^ "\nPGIP error occured in XML text below:\n" ^
  1317                     (XML.string_of_tree xml)))
  1318 
  1319 val process_pgip = K () o process_pgip_tree o XML.tree_of_string
  1320 
  1321 end
  1322 
  1323 
  1324 (* PGIP loop: process PGIP input only *)
  1325 
  1326 local
  1327 
  1328 exception XML_PARSE
  1329 
  1330 fun loop ready src =
  1331     let
  1332         val _ = if ready then (issue_pgipe "ready" []) else ()
  1333         val pgipo = (Source.get_single src)
  1334                         handle e => raise XML_PARSE
  1335     in
  1336         case pgipo of
  1337              NONE  => ()
  1338            | SOME (pgip,src') =>
  1339              let
  1340                  val ready' = (process_pgip_tree pgip) handle e => (handler (e,SOME src'); true)
  1341              in
  1342                  loop ready' src'
  1343              end
  1344     end handle e => handler (e,SOME src)  (* i.e. error in ready/XML parse *)
  1345 
  1346 and handler (e,srco) =
  1347     case (e,srco) of
  1348         (XML_PARSE,SOME src) =>
  1349         Output.panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *)
  1350       | (PGIP_QUIT,_) => ()
  1351       | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src)
  1352       | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *)
  1353       | (e,SOME src) => (error (Toplevel.exn_message e); loop true src)
  1354       | (_,NONE) => ()
  1355 in
  1356   (* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *)
  1357 
  1358   val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
  1359 
  1360   val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
  1361 
  1362   fun pgip_toplevel x = loop true x
  1363 end
  1364 
  1365 
  1366 (* additional outer syntax for Isar *)
  1367 
  1368 local structure P = OuterParse and K = OuterKeyword in
  1369 
  1370 val undoP = (*undo without output*)
  1371   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
  1372     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
  1373 
  1374 val redoP = (*redo without output*)
  1375   OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
  1376     (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
  1377 
  1378 val context_thy_onlyP =
  1379   OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
  1380     (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
  1381 
  1382 val try_context_thy_onlyP =
  1383   OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
  1384     (P.name >> (Toplevel.no_timing oo
  1385       (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
  1386 
  1387 val restartP =
  1388   OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
  1389     (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
  1390 
  1391 val kill_proofP =
  1392   OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
  1393     (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
  1394 
  1395 val inform_file_processedP =
  1396   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
  1397     (P.name >> (fn file => Toplevel.no_timing o
  1398       Toplevel.keep (vacuous_inform_file_processed file) o
  1399       Toplevel.kill o
  1400       Toplevel.keep (proper_inform_file_processed file)));
  1401 
  1402 val inform_file_retractedP =
  1403   OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
  1404     (P.name >> (Toplevel.no_timing oo
  1405       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
  1406 
  1407 val process_pgipP =
  1408   OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
  1409     (P.text >> (Toplevel.no_timing oo
  1410       (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
  1411 
  1412 fun init_outer_syntax () = OuterSyntax.add_parsers
  1413  [undoP, redoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
  1414   inform_file_processedP, inform_file_retractedP, process_pgipP];
  1415 
  1416 end;
  1417 
  1418 
  1419 (* init *)
  1420 
  1421 val initialized = ref false;
  1422 
  1423 fun set_prompts true _ = ml_prompts "ML> " "ML# "
  1424   | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
  1425   | set_prompts false false = ml_prompts ("> " ^ special "372") ("- " ^ special "373");
  1426 
  1427 fun init_setup isar pgip =
  1428   (conditional (not (! initialized)) (fn () =>
  1429    (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
  1430     setup_xsymbols_output ();
  1431     setup_pgml_output ();
  1432     setup_messages ();
  1433     setup_state ();
  1434     setup_thy_loader ();
  1435     setup_present_hook ();
  1436     set initialized; ()));
  1437   sync_thy_loader ();
  1438   change print_mode (cons proof_generalN o remove (op =) proof_generalN);
  1439   init_pgip_session_id ();
  1440   if pgip then
  1441     change print_mode (append [pgmlN, pgmlatomsN] o subtract (op =) [pgmlN, pgmlatomsN])
  1442   else
  1443     pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
  1444   set_prompts isar pgip;
  1445   pgip_active := pgip);
  1446 
  1447 fun init isar =
  1448  (init_setup isar false;
  1449   if isar then Isar.sync_main () else isa_restart ());
  1450 
  1451 fun init_pgip false = Output.panic "PGIP not supported for Isabelle/classic mode."
  1452   | init_pgip true = (init_setup true true; pgip_toplevel tty_src);
  1453 
  1454 
  1455 
  1456 (** generate elisp file for keyword classification **)
  1457 
  1458 local
  1459 
  1460 val regexp_meta = explode ".*+?[]^$";
  1461 val regexp_quote =
  1462   implode o map (fn c => if c mem_string regexp_meta then "\\\\" ^ c else c) o explode;
  1463 
  1464 fun defconst name strs =
  1465   "\n(defconst isar-keywords-" ^ name ^
  1466   "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
  1467 
  1468 fun make_elisp_commands commands kind = defconst kind
  1469   (commands |> map_filter (fn (c, _, k, _) => if k = kind then SOME c else NONE));
  1470 
  1471 fun make_elisp_syntax (keywords, commands) =
  1472   ";;\n\
  1473   \;; Keyword classification tables for Isabelle/Isar.\n\
  1474   \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
  1475   \;;\n\
  1476   \;; $" ^ "Id$\n\
  1477   \;;\n" ^
  1478   defconst "major" (map #1 commands) ^
  1479   defconst "minor" (List.filter Syntax.is_identifier keywords) ^
  1480   implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
  1481   "\n(provide 'isar-keywords)\n";
  1482 
  1483 in
  1484 
  1485 fun write_keywords s =
  1486  (init_outer_syntax ();
  1487   File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
  1488     (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
  1489 
  1490 end;
  1491 
  1492 end;