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