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