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