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