src/Pure/proof_general.ML

tuned Isar interfaces;
tuned IsarThy.theorem_i;

(*  Title:      Pure/proof_general.ML
    ID:         $Id$
    Author:     David Aspinall and Markus Wenzel

Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk)
Includes support for PGIP control language for Isabelle/Isar.

===========================================================================
NOTE: With this version you will lose support for the Isabelle
settings menu in the currently released version of Proof General (3.5).
No other changes should be visible in the Emacs interface.

The 3.6pre pre-release versions of Emacs Proof General now support the
new PGIP format for preferences and restore the settings menu.
Please visit http://proofgeneral.inf.ed.ac.uk/develdownload
===========================================================================

STATUS: this version is an experimental version that supports PGIP 2.X.
*)

signature PROOF_GENERAL =
sig
  val update_thy_only: string -> unit
  val try_update_thy_only: string -> unit
  val inform_file_retracted: string -> unit
  val inform_file_processed: string -> unit
  val preferences:
      (string *
        (string *
         (string *
          (string * (string * (unit -> string)) *
           (string -> unit)))) list) list ref
  val process_pgip: string -> unit
  val thms_containing: string list -> unit
  val help: unit -> unit
  val show_context: unit -> theory
  val kill_goal: unit -> unit
  val repeat_undo: int -> unit
  val isa_restart: unit -> unit
  val full_proofs: bool -> unit
  val isarcmd: string -> unit
  val init: bool -> unit
  val init_pgip: bool -> unit
  val write_keywords: string -> unit
  val xmls_of_str: string -> string list   (*temp for testing parser*)
end;

structure ProofGeneral: PROOF_GENERAL =
struct

structure P = OuterParse;


(* PGIP messaging mode (independent of PGML output) *)

val pgip_active = ref false;
val pgip_emacs_compatibility_flag = ref false;

fun pgip () = (! pgip_active);
fun pgip_emacs_compatibility () = (! pgip_emacs_compatibility_flag);


(* print modes *)

val proof_generalN = "ProofGeneral";  (*token markup (colouring vars, etc.)*)
val pgasciiN = "PGASCII";             (*plain 7-bit ASCII communication*)
val xsymbolsN = Symbol.xsymbolsN;     (*X-Symbol symbols*)
val pgmlN = "PGML";                   (*XML escapes and PGML symbol elements*)
val pgmlatomsN = "PGMLatoms";         (*variable kind decorations*)
val thm_depsN = "thm_deps";           (*meta-information about theorem deps*)

fun pgml () = Output.has_mode pgmlN;

fun special oct =
  if Output.has_mode pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
  else oct_char oct;


(* text output: print modes for xsymbol and PGML *)

local

fun xsym_output "\\" = "\\\\"
  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;

fun xsymbols_output s =
  if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then
    let val syms = Symbol.explode s
    in (implode (map xsym_output syms), real (Symbol.length syms)) end
  else Symbol.default_output s;

fun pgml_sym s =
  (case Symbol.decode s of
    (*NB: an alternative here would be to output the default print mode alternative
      in the element content, but unfortunately print modes are not that fine grained.*)
    Symbol.Char s => XML.text s
  | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
  | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *)
  | Symbol.Raw s => s);

fun pgml_output str =
  let val syms = Symbol.explode str
  in (implode (map pgml_sym syms), real (Symbol.length syms)) end;

in

fun setup_xsymbols_output () =
  Output.add_mode xsymbolsN
    (xsymbols_output, Symbol.default_indent, Symbol.encode_raw);

fun setup_pgml_output () =
  Output.add_mode pgmlN
    (pgml_output, Symbol.default_indent, Symbol.encode_raw);

end;


(* token translations *)

local

fun end_tag () = special "350";
val class_tag = ("class", fn () => special "351");
val tfree_tag = ("tfree", fn () => special "352");
val tvar_tag = ("tvar", fn () => special "353");
val free_tag = ("free", fn () => special "354");
val bound_tag = ("bound", fn () => special "355");
val var_tag = ("var", fn () => special "356");
val skolem_tag = ("skolem", fn () => special "357");

fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];

fun tagit (kind, bg_tag) x =
 (if Output.has_mode pgmlatomsN then xml_atom kind x
  else bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));

fun free_or_skolem x =
  (case try Syntax.dest_skolem x of
    NONE => tagit free_tag x
  | SOME x' => tagit skolem_tag x');

fun var_or_skolem s =
  (case Syntax.read_variable s of
    SOME (x, i) =>
      (case try Syntax.dest_skolem x of
        NONE => tagit var_tag s
      | SOME x' => tagit skolem_tag
          (setmp show_question_marks true Syntax.string_of_vname (x', i)))
  | NONE => tagit var_tag s);

val proof_general_trans =
 Syntax.tokentrans_mode proof_generalN
  [("class", tagit class_tag),
   ("tfree", tagit tfree_tag),
   ("tvar", tagit tvar_tag),
   ("free", free_or_skolem),
   ("bound", tagit bound_tag),
   ("var", var_or_skolem)];

in

val _ = Context.add_setup [Theory.add_tokentrfuns proof_general_trans];

end;


(* assembling PGIP packets *)

val pgip_refid  = ref NONE: string option ref;
val pgip_refseq = ref NONE: string option ref;

local
  val pgip_class  = "pg"
  val pgip_tag = "Isabelle/Isar"
  val pgip_id = ref ""
  val pgip_seq = ref 0
  fun pgip_serial () = inc pgip_seq

  fun assemble_pgips pgips =
    XML.element
      "pgip"
      ([("tag",    pgip_tag),
        ("class",  pgip_class),
        ("seq",    string_of_int (pgip_serial())),
        ("id",     !pgip_id)] @
       if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
       (* destid=refid since Isabelle only communicates back to sender,
          so we may omit refid from attributes.
       if_none (Option.map (single o (pair "refid"))  (! pgip_refid)) [] @
       *)
       if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) [])
      pgips;

in

fun init_pgip_session_id () =
    pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
               getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())


fun matching_pgip_id id = (id = !pgip_id)

fun decorated_output bg en prfx =
  writeln_default o enclose bg en o prefix_lines prfx;

(* FIXME: see Rev 1.48 [PG CVS] for cleaner version of this which can be used
   for PG 4.0 which processes PGIP without needing special chars *)
fun issue_pgips ps =
  if pgip_emacs_compatibility() then
    decorated_output (*add urgent message annotation*)
      (special "360") (special "361") ""
      (assemble_pgips ps)
  else
    writeln_default (assemble_pgips ps);

fun assemble_pgip resp attrs s = assemble_pgips [XML.element resp attrs [s]];
fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []];

(* FIXME: need to add stuff to gather PGIPs here *)
fun issue_pgip resp attrs txt =
  if pgip_emacs_compatibility () then
    decorated_output (*add urgent message annotation*)
      (special "360") (special "361") ""
      (assemble_pgip resp attrs txt)
  else
    writeln_default (assemble_pgip resp attrs txt);

(* FIXME: temporarily to support PG 3.4 *)
fun issue_pgip_maybe_decorated bg en resp attrs s =
  if pgip_emacs_compatibility () then
    (*in PGIP mode, but using escape characters as well*)
    writeln_default (enclose bg en (assemble_pgip resp attrs s))
  else
    issue_pgip resp attrs s;

fun issue_pgipe resp attrs = writeln_default (assemble_pgipe resp attrs);

end;


(* messages and notification *)

local
  val delay_msgs = ref false;   (*true: accumulate messages*)
  val delayed_msgs = ref [];
in

fun message resp attrs bg en prfx s =
  if pgip () then
   (if (! delay_msgs) then
      delayed_msgs := (resp, attrs, prefix_lines prfx s) :: ! delayed_msgs (*NB: no decs*)
    else
      issue_pgip_maybe_decorated bg en resp attrs
        (XML.element "pgmltext" [] [prefix_lines prfx s]))
  else decorated_output bg en prfx s;

fun start_delay_msgs () = (set delay_msgs; delayed_msgs := []);

fun end_delayed_msgs () = (reset delay_msgs;
  (! delayed_msgs) |> map (fn (resp, attrs, s) =>
    XML.element resp attrs [XML.element "pgmltext" [] [s]]));

end;

local
  val display_area = ("area", "display");
  val message_area = ("area", "message");
  val internal_category = ("messagecategory", "internal");
  val info_category = ("messagecategory", "information");
  val tracing_category = ("messagecategory", "tracing");
  val urgent_indication = ("urgent", "y");
  val nonfatal = ("fatality", "nonfatal");
  val fatal = ("fatality", "fatal");
  val panic = ("fatality", "panic");

  val thyname_attr = pair "thyname";
  val url_attr = pair "url";
  fun localfile_url_attr path = url_attr ("file:///" ^ path);
in

fun setup_messages () =
 (writeln_fn := (fn s => message "normalresponse" [message_area] "" "" "" s);
  priority_fn := (fn s => message "normalresponse" [message_area, urgent_indication]
    (special "360") (special "361") "" s);
  tracing_fn := (fn s => message "normalresponse"  [message_area, tracing_category]
    (special "360" ^ special "375") (special "361") "" s);
  info_fn := (fn s => message "normalresponse" [message_area, info_category]
    (special "362") (special "363") "+++ " s);
  debug_fn := (fn s => message "normalresponse" [message_area, internal_category]
    (special "362") (special "363") "+++ " s);
  warning_fn := (fn s => message "errorresponse" [nonfatal]
    (special "362") (special "363") "### " s);
  error_fn := (fn s => message "errorresponse" [fatal]
    (special "364") (special "365") "*** " s);
  panic_fn := (fn s => message "errorresponse" [panic]
    (special "364") (special "365") "!!! " s));


(* accumulate printed output in a single PGIP response (inside <pgmltext>) *)

fun with_displaywrap (elt, attrs) dispfn =
  let
    val lines = ref ([]: string list);
    fun wlgrablines s = lines := s :: ! lines;
  in
    setmp writeln_fn wlgrablines dispfn ();
    (* IMPORTANT FIXME: XML.element here too inefficient, should use stream output *)
    issue_pgip elt attrs (XML.element "pgmltext" [] (! lines))
  end;

fun emacs_notify s = decorated_output (special "360") (special "361") "" s;

fun tell_clear_goals () =
  if pgip () then
    issue_pgipe "cleardisplay" [display_area]
  else
    emacs_notify "Proof General, please clear the goals buffer.";

fun tell_clear_response () =
  if pgip () then
    issue_pgipe "cleardisplay" [message_area]
  else
    emacs_notify "Proof General, please clear the response buffer.";

fun tell_file_loaded path =
  if pgip () then
    issue_pgipe "informfileloaded"
      [localfile_url_attr  (XML.text (File.platform_path path))]
  else
    emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));

fun tell_file_retracted path =
  if pgip() then
    issue_pgipe "informfileretracted"
      [localfile_url_attr  (XML.text (File.platform_path path))]
  else
    emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));


(* theory / proof state output *)

local

fun tmp_markers f =
  setmp Display.current_goals_markers (special "366", special "367", "") f ();

fun statedisplay prts =
  issue_pgip "proofstate" []
    (XML.element "pgml" []
      [XML.element "statedisplay" [] [Pretty.output (Pretty.chunks prts)]]);

fun print_current_goals n m st =
  if pgml () then statedisplay (Display.pretty_current_goals n m st)
  else tmp_markers (fn () => Display.print_current_goals_default n m st);

fun print_state b st =
  if pgml () then statedisplay (Toplevel.pretty_state b st)
  else tmp_markers (fn () => Toplevel.print_state_default b st);

in

fun setup_state () =
  (Display.print_current_goals_fn := print_current_goals;
   Toplevel.print_state_fn := print_state;
   (* FIXME: check next octal char won't appear in pgip? *)
   Toplevel.prompt_state_fn := (fn s => suffix (special "372")
     (Toplevel.prompt_state_default s)));

end;

end;


(* misc commands for ProofGeneral/isa *)

fun thms_containing ss =
  FindTheorems.print_theorems (ProofContext.init (the_context ())) NONE NONE
    (map (fn s => (true, FindTheorems.Pattern s)) ss);

val welcome = priority o Session.welcome;
val help = welcome;
val show_context = Context.the_context;

fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());

fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;

fun repeat_undo 0 = ()
  | repeat_undo 1 = undo ()
  | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));


(* theory loader actions *)

local

fun add_master_files name files =
  let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
  in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;

fun trace_action action name =
  if action = ThyInfo.Update then
    List.app tell_file_loaded (ThyInfo.loaded_files name)
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
    List.app tell_file_retracted (add_master_files name (ThyInfo.loaded_files name))
  else ();

in
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
end;


(* prepare theory context *)

val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;

(* FIXME general treatment of tracing*)
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;

fun dynamic_context () =
  (case Context.get_context () of
    SOME thy => "  Using current (dynamic!) one: " ^ quote (Context.theory_name thy)
  | NONE => "");

fun try_update_thy_only file =
  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
    let val name = thy_name file in
      if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
      then update_thy_only name
      else warning ("Unkown theory context of ML file." ^ dynamic_context ())
    end) ();


(* get informed about files *)

val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;

fun proper_inform_file_processed file state =
  let val name = thy_name file in
    if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
     (ThyInfo.touch_child_thys name;
      transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
       (warning msg; warning ("Failed to register theory: " ^ quote name);
        tell_file_retracted (Path.base (Path.unpack file))))
    else raise Toplevel.UNDEF
  end;

fun vacuous_inform_file_processed file state =
 (warning ("No theory " ^ quote (thy_name file));
  tell_file_retracted (Path.base (Path.unpack file)));


(* restart top-level loop (keeps most state information) *)

local

fun restart isar =
 (if isar then tell_clear_goals () else kill_goal ();
  tell_clear_response ();
  welcome ());

in

fun isa_restart () = restart false;
fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);

end;

fun full_proofs true = proofs := 2
  | full_proofs false = proofs := 1;


(* theorem dependency output *)

local

val spaces_quote = space_implode " " o map quote;

(* FIXME: investigate why dependencies at the moment include themselves! *)
fun thm_deps_message (thms, deps) =
  if pgip() then
    issue_pgips
      [XML.element
        "metainforesponse"  (* FIXME: get thy name from info here? *)
        [("infotype", "isabelle_theorem_dependencies")]
        [XML.element "value" [("name", "thms")] [XML.text thms],
         XML.element "value" [("name", "deps")] [XML.text deps]]]
  else emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);

fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
  let
    val names = filter_out (equal "") (map Thm.name_of_thm ths);
    val deps = filter_out (equal "")
      (Symtab.keys (fold Proofterm.thms_of_proof
        (map Thm.proof_of ths) Symtab.empty));
  in
    if null names orelse null deps then ()
    else thm_deps_message (spaces_quote names, spaces_quote deps)
  end);

in

fun setup_present_hook () =
  Present.add_hook (fn _ => fn res => tell_thm_deps (List.concat (map #2 res)));

end;



(** preferences **)

local

val pgipnat = XML.element "pgipint" [("min", "0")] [];
fun pgipnatmax max = XML.element "pgipint" [("min", "0"), ("max", string_of_int max)] [];
val pgipbool = XML.element "pgipbool" [] [];

fun with_default f = (f (), f);

in

fun nat_option r = (pgipnat,
  with_default (fn () => string_of_int (! r)),
  (fn s => (case Syntax.read_nat s of
      NONE => error ("nat_option: illegal value: " ^ s)
    | SOME i => r := i)));

fun bool_option r = (pgipbool,
  with_default (fn () => Bool.toString (! r)),
  (fn "false" => r := false | "true" => r := true
    | x => error ("bool_option: illegal value: " ^ x)));

val proof_option = (pgipbool,
  with_default (fn () => Bool.toString (! proofs >= 2)),
  (fn "false" => proofs := 1 | "true" => proofs := 2
    | x => error ("proof_option: illegal value: " ^ x)));

val thm_deps_option = (pgipbool,
  with_default (fn () => Bool.toString (Output.has_mode thm_depsN)),
  (fn "false" => change print_mode (remove (op =) thm_depsN)
    | "true" => change print_mode (insert (op =) thm_depsN)
    | x => error ("thm_deps_option: illegal value: " ^ x)));

local
  val pg_print_depth_val = ref 10;
  fun pg_print_depth n = (print_depth n; pg_print_depth_val := n)
in

val print_depth_option = (pgipnat,
  with_default (fn () => string_of_int (! pg_print_depth_val)),
  (fn s => (case Syntax.read_nat s of
      NONE => error ("print_depth_option: illegal value: " ^ s)
    | SOME i => pg_print_depth i)));
end;

val preferences = ref
  [("Display",
    [("show-types",
      ("Include types in display of Isabelle terms",
       bool_option show_types)),
     ("show-sorts",
      ("Include sorts in display of Isabelle terms",
       bool_option show_sorts)),
     ("show-consts",
      ("Show types of consts in Isabelle goal display",
       bool_option show_consts)),
     ("long-names",
      ("Show fully qualified names in Isabelle terms",
       bool_option long_names)),
     ("show-brackets",
      ("Show full bracketing in Isabelle terms",
       bool_option show_brackets)),
     ("show-main-goal",
      ("Show main goal in proof state display",
       bool_option Proof.show_main_goal)),
     ("eta-contract",
      ("Print terms eta-contracted",
       bool_option Syntax.eta_contract))]),
   ("Advanced Display",
    [("goals-limit",
      ("Setting for maximum number of goals printed",
       nat_option goals_limit)),
     ("prems-limit",
      ("Setting for maximum number of premises printed",
       nat_option ProofContext.prems_limit)),
     ("print-depth",
      ("Setting for the ML print depth",
       print_depth_option)),
     ("show-question-marks",
      ("Show leading question mark of variable name",
       bool_option show_question_marks))]),
   ("Tracing",
    [("trace-simplifier",
      ("Trace simplification rules.",
       bool_option trace_simp)),
     ("trace-rules",
      ("Trace application of the standard rules",
       bool_option trace_rules)),
     ("trace-unification",
      ("Output error diagnostics during unification",
       bool_option Pattern.trace_unify_fail)),
     ("global-timing",
      ("Whether to enable timing in Isabelle.",
       bool_option Output.timing))]),
   ("Proof",
    [("quick-and-dirty",
      ("Take a few short cuts",
       bool_option quick_and_dirty)),
     ("full-proofs",
      ("Record full proof objects internally",
       proof_option)),
     ("theorem-dependencies",
       ("Track theorem dependencies within Proof General",
        thm_deps_option)),
     ("skip-proofs",
      ("Ignore proof scripts (interactive-only)",
       bool_option Toplevel.skip_proofs))])
   ];
end;


(* Configuration: GUI config, proverinfo messages *)

local
    val config_file = "~~/lib/ProofGeneral/pgip_isar.xml"
    val name_attr = pair "name"
    val version_attr = pair "version"
    val isabelle_www = "http://isabelle.in.tum.de/"
in
fun send_pgip_config () =
    let
        val path = Path.unpack config_file
        val exists = File.exists path
        val proverinfo =
            XML.element "proverinfo"
              [("name",Session.name()), ("version", version),
               ("url", isabelle_www), ("filenameextns", ".thy;")]
            [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
             XML.element "helpdoc"
         (* NB: would be nice to generate/display docs from isatool
          doc, but that program may not be running on same machine;
          front end should be responsible for launching viewer, etc. *)
                      [("name", "Isabelle/HOL Tutorial"),
                       ("descr", "A Gentle Introduction to Isabelle/HOL"),
                       ("url",  "http://isabelle.in.tum.de/dist/Isabelle2004/doc/tutorial.pdf")]
              []]
    in
        if exists then
            (issue_pgips [proverinfo]; issue_pgips [File.read path])
        else panic ("PGIP configuration file " ^ config_file ^ " not found")
    end;
end


(* Reveal some information about prover state *)
fun send_informguise (openfile, opentheory, openproofpos) =
    let val guisefile =
            case openfile of SOME f => [XML.element "guisefile"
                                                    [("url",Url.pack (Url.File (Path.unpack f)))] []]
                           | _ => []
        val guisetheory =
            case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
                             | _ => []
        val guiseproof =
            case openproofpos of SOME i => [XML.element "guiseproof" [("proofpos", string_of_int i)] []]
                               | _ => []
    in
        issue_pgips [XML.element "informguise" [] (guisefile @ guisetheory @ guiseproof)]
    end


(* PGIP identifier tables (prover objects). [incomplete] *)

local
    val objtype_thy  = "theory"
    val objtype_thm  = "theorem"
    val objtype_term = "term"
    val objtype_type = "type"

    fun xml_idtable ty ctx ids =
        let
            fun ctx_attr (SOME c)= [("context", c)]
              | ctx_attr NONE    = []
            fun xmlid x = XML.element "identifier" [] [XML.text x];
        in
            XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
                                  (map xmlid ids)
        end
in

fun setids t = issue_pgip "setids" [] t
fun addids t = issue_pgip "addids" [] t
fun delids t = issue_pgip "delids" [] t

fun delallids ty = setids (xml_idtable ty NONE [])

fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
fun clear_thy_idtable () = delallids objtype_thy

fun send_thm_idtable ctx thy =
    addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy)));

fun clear_thm_idtable () = delallids objtype_thm

(* fun send_type_idtable thy = TODO, it's a bit low-level messy
   & maybe not so useful anyway *)

end

(* Response to interface queries about known objects *)

local
 val topthy = Toplevel.theory_of o Toplevel.get_state
 fun pthm thy name = print_thm (get_thm thy (Name name))

 fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
in
(* FIXME: add askids for "file" here, which returns single theory with same name *)
fun askids (NONE, SOME "theory")  = send_thy_idtable NONE (ThyInfo.names())
  | askids (NONE, NONE) =  send_thy_idtable NONE (ThyInfo.names())
                           (* only theories known in top context *)
  | askids (SOME thy, SOME "theory") = send_thy_idtable (SOME thy) (ThyInfo.get_preds thy)
  | askids (SOME thy, SOME "theorem") = send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)
  | askids (SOME thy, NONE) = (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy);
                               send_thm_idtable (SOME thy) (ThyInfo.get_theory thy))
  | askids (_, SOME ot) = error ("No objects of type "^(quote ot)^" are available here.")

fun showid (_,        "theory", n) =
    with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
  | showid (SOME thy, "theorem", t) =
    with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
  | showid (NONE,     "theorem", t) =
    with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t)
  | showid (_, ot, _) = error ("Cannot show objects of type "^ot)

end


(** Parsing proof scripts without execution **)

(* Notes.
   This is quite tricky, because 1) we need to put back whitespace which
   was removed during parsing so we can provide markup around commands;
   2) parsing is intertwined with execution in Isar so we have to repeat
   the parsing to extract interesting parts of commands.  The trace of
   tokens parsed which is now recorded in each transition (added by
   Markus June '04) helps do this, but the mechanism is still a bad mess.

   If we had proper parse trees it would be easy, although having a
   fixed type of trees might be tricky with Isar's extensible parser.

   Probably the best solution is to produce the meta-information at
   the same time as the parse, for each command, e.g. by recording a
   list of (name,objtype) pairs which record the bindings created by
   a command.  This would require changing the interfaces in
   outer_syntax.ML (or providing new ones),

    datatype metainfo = Binding of string * string  (* name, objtype *)

    val command_withmetainfo: string -> string -> string ->
      (token list ->
       ((Toplevel.transition -> Toplevel.transition) * metainfo list) *
       token list) -> parser

   We'd also like to render terms as they appear in output, but this
   will be difficult because inner syntax is extensible and we don't
   have the correct syntax to hand when just doing outer parsing
   without execution.  A reasonable approximation could
   perhaps be obtained by using the syntax of the current context.
   However, this would mean more mess trying to pick out terms,
   so at this stage a more serious change to the Isar functions
   seems necessary.
*)

local
    fun markup_text str elt = [XML.element elt [] [XML.text str]]
    fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
    fun empty elt = [XML.element elt [] []]

    fun whitespace str = XML.element "whitespace" [] [XML.text str]

    (* an extra token is needed to terminate the command *)
    val sync = OuterSyntax.scan "\\<^sync>";

    fun named_item_elt_with nameattr toks str elt nameP objtyp =
        let
            val name = (fst (nameP (toks@sync)))
                        handle _ => (error ("Error occurred in name parser for " ^ elt ^
                                            "(objtype: " ^ objtyp ^ ")");
                                     "")

        in
            [XML.element elt
                         ((if name="" then [] else [(nameattr, name)])@
                          (if objtyp="" then [] else [("objtype", objtyp)]))
                         ([XML.text str])]
        end

    val named_item_elt = named_item_elt_with "name"
    val thmnamed_item_elt = named_item_elt_with "thmname"

    fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg)

    (* FIXME: allow dynamic extensions to language here: we need a hook in
       outer_syntax.ML to reset this table. *)

    val keywords_classification_table = ref (NONE: string Symtab.table option)

    fun get_keywords_classification_table () =
        case (!keywords_classification_table) of
          SOME t => t
        | NONE => (let
                     val tab = fold (fn (c, _, k, _) => Symtab.curried_update (c, k))
                                    (OuterSyntax.dest_parsers ()) Symtab.empty;
                   in (keywords_classification_table := SOME tab; tab) end)



    fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
        let
            val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
        in
            markup_text_attrs str "opentheory"
                              ([("thyname",thyname)] @
                               (if imports=[] then [] else
                                [("parentnames", (space_implode ";" imports) ^ ";")]))
        end

    fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)
        let
            (* NB: PGIP only deals with single name bindings at the moment;
               potentially we could markup grouped definitions several times but
               that might suggest the wrong structure to the editor?
               Better alternative would be to put naming closer around text,
               but to do that we'd be much better off modifying the real parser
               instead of reconstructing it here. *)

            val plain_items = (* no names, unimportant names, or too difficult *)
                ["defaultsort","arities","judgement","finalconsts",
                 "syntax", "nonterminals", "translations",
                 "global", "local", "hide",
                 "ML_setup", "setup", "method_setup",
                 "parse_ast_translation", "parse_translation", "print_translation",
                 "typed_print_translation", "print_ast_translation", "token_translation",
                 "oracle",
                 "declare"]

            val plain_item   = markup_text str "theoryitem"
            val comment_item = markup_text str "litcomment"
            val named_item   = named_item_elt toks str "theoryitem"

            val opt_overloaded = P.opt_keyword "overloaded";

            val thmnameP = (* see isar_syn.ML/theoremsP *)
                let
                    val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
                    val theoremsP = P.opt_locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
                in
                    theoremsP
                end
        in
            (* TODO: ideally we would like to render terms properly, just as they are
               in output. This implies using PGML for symbols and variables/atoms.
               BUT it's rather tricky without having the correct concrete syntax to hand,
               and even if we did, we'd have to mess around here a whole lot more first
               to pick out the terms from the syntax. *)

            if (name mem plain_items) then plain_item
            else case name of
                     "text"      => comment_item
                   | "text_raw"  => comment_item
                   | "typedecl"  => named_item (P.type_args |-- P.name) "type"
                   | "types"     => named_item (P.type_args |-- P.name) "type"
                   | "classes"   => named_item P.name "class"
                   | "classrel"  => named_item P.name "class"
                   | "consts"    => named_item (P.const >> #1) "term"
                   | "axioms"    => named_item (P.spec_name >> (#1 o #1)) "theorem"
                   | "defs"      => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
                   | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
                   | "theorems"  => named_item thmnameP "thmset"
                   | "lemmas"    => named_item thmnameP "thmset"
                   | "oracle"    => named_item P.name "oracle"
                   | "locale"    => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
                   | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item)
        end

    fun xmls_of_thy_goal (name,toks,str) =
        let
            (* see isar_syn.ML/gen_theorem *)
         val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
         val general_statement =
            statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);

            val gen_theoremP =
                P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
                 Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
                                 general_statement >> (fn ((locale, a), (elems, concl)) =>
                                                         fst a) (* a : (bstring * Args.src list) *)

            val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
            (* TODO: add preference values for attributes
               val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
            *)
        in
            (thmnamed_item_elt toks str "opengoal" nameP "") @
            (empty "openblock")
        end

    fun xmls_of_qed (name,markup) =
        let val qedmarkup  =
                (case name of
                     "sorry" => markup "postponegoal"
                   | "oops"  => markup "giveupgoal"
                   | "done"  => markup "closegoal"
                   | "by"    => markup "closegoal"  (* nested or toplevel *)
                   | "qed"   => markup "closegoal"  (* nested or toplevel *)
                   | "."     => markup "closegoal"  (* nested or toplevel *)
                   | ".."    => markup "closegoal"  (* nested or toplevel *)
                   | other => (* default to closegoal: may be wrong for extns *)
                                  (parse_warning
                                       ("Unrecognized qed command: " ^ quote other);
                                       markup "closegoal"))
        in qedmarkup @ (empty "closeblock") end

    fun xmls_of_kind kind (name,toks,str) =
    let val markup = markup_text str in
    case kind of
      "control"        => markup "badcmd"
    | "diag"           => markup "spuriouscmd"
    (* theory/files *)
    | "theory-begin"   => xmls_of_thy_begin (name,toks,str)
    | "theory-decl"    => xmls_of_thy_decl (name,toks,str)
    | "theory-heading" => markup "litcomment"
    | "theory-script"  => markup "theorystep"
    | "theory-end"     => markup "closetheory"
    (* proof control *)
    | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
    | "proof-heading"  => markup "litcomment"
    | "proof-goal"     => (markup "opengoal") @ (empty "openblock")  (* nested proof: have, show, ... *)
    | "proof-block"    => markup "proofstep" (* context-shift: proof, next; really "newgoal" *)
    | "proof-open"     => (empty "openblock") @ (markup "proofstep")
    | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
    | "proof-script"   => markup "proofstep"
    | "proof-chain"    => markup "proofstep"
    | "proof-decl"     => markup "proofstep"
    | "proof-asm"      => markup "proofstep"
    | "proof-asm-goal" => (markup "opengoal") @ (empty "openblock")  (* nested proof: obtain *)
    | "qed"            => xmls_of_qed (name,markup)
    | "qed-block"      => xmls_of_qed (name,markup)
    | "qed-global"     => xmls_of_qed (name,markup)
    | other => (* default for anything else is "spuriouscmd", ignored for undo. *)
      (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other);
       markup "spuriouscmd")
    end
in

fun xmls_of_transition (name,str,toks) =
   let
     val classification = Symtab.curried_lookup (get_keywords_classification_table ()) name
   in case classification of
          SOME k => (xmls_of_kind k (name,toks,str))
        | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
          (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
           markup_text str "spuriouscmd")
   end

fun markup_toks [] _ = []
  | markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x

fun markup_comment_whs [] = []
  | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
    let
        val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
    in
        if (prewhs <> []) then
            whitespace (implode (map OuterLex.unparse prewhs))
            :: (markup_comment_whs rest)
        else
            (markup_text (OuterLex.unparse t) "comment") @
            (markup_comment_whs ts)
    end

fun xmls_pre_cmd [] = ([],[])
  | xmls_pre_cmd toks =
    let
        (* an extra token is needed to terminate the command *)
        val sync = OuterSyntax.scan "\\<^sync>";
        val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode
        val text_with_whs =
            ((spaceP || Scan.succeed "") --
             (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^)
             -- (spaceP || Scan.succeed "") >> op^
        val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync)
        (* NB: this collapses  litcomment,(litcomment|whitespace)* to a single litcomment *)
        val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1
        val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2
    in
        ((markup_comment_whs prewhs) @
         (if (length rest2 = length rest1)  then []
          else markup_text (implode
                                (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1))))
               "litcomment") @
         (markup_comment_whs postwhs),
         Library.take (length rest3 - 1,rest3))
    end

fun xmls_of_impropers toks =
    let
        val (xmls,rest) = xmls_pre_cmd toks
    in
        xmls @ (markup_toks rest "unparseable")
    end

fun markup_unparseable str = markup_text str "unparseable"

end


local
    (* we have to weave together the whitespace/comments with proper tokens
       to reconstruct the input. *)
    (* TODO: see if duplicating isar_output/parse_thy can help here *)

    fun match_tokens ([],us,vs) = (rev vs,us)  (* used, unused *)
      | match_tokens (t::ts,w::ws,vs) =
        if (t = w) then match_tokens (ts,ws,w::vs)
        else match_tokens (t::ts,ws,w::vs)
      | match_tokens _ = error ("match_tokens: mismatched input parse")
in
    fun xmls_of_str str =
    let
       (* parsing:   See outer_syntax.ML/toplevel_source *)
       fun parse_loop ([],[],xmls) = xmls
         | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
         | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
           let
               (* first proper token after whitespace/litcomment/whitespace is command *)
               val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
               val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
                                                     | _ => error("proof_general/parse_loop impossible")
               val (utoks,itoks'') = match_tokens (toks,itoks',[])
               (* FIXME: should take trailing [w/s+] semicolon too in utoks *)

               val str = implode (map OuterLex.unparse (cmdtok::utoks))

               val xmls_tr  = xmls_of_transition (nm,str,toks)
           in
               parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr)
           end
    in
        (let val toks = OuterSyntax.scan str
         in
             parse_loop (OuterSyntax.read toks, toks, [])
         end)
           handle _ => markup_unparseable str
    end


fun parsescript str attrs =
    let
        val _ = start_delay_msgs ()  (* accumulate error messages to put inside parseresult *)
        val xmls = xmls_of_str str
        val errs = end_delayed_msgs ()
     in
        issue_pgips [XML.element "parseresult" attrs (errs@xmls)]
    end
end



(**** PGIP:  Isabelle -> Interface ****)

val isabelle_pgml_version_supported = "1.0";
val isabelle_pgip_version_supported = "2.0"

(* TODO: would be cleaner to define a datatype here for the accepted elements,
   and mapping functions to/from strings.  At the moment this list must
   coincide with the strings in the function process_pgip_element. *)
val isabelle_acceptedpgipelems =
    ["askpgip","askpgml","askprefs","getpref","setpref",
     "proverinit","proverexit","startquiet","stopquiet",
     "pgmlsymbolson", "pgmlsymbolsoff",
     "dostep", "undostep", "redostep", "abortgoal", "forget", "restoregoal",
     "askids", "showid", "askguise",
     "parsescript",
     "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
     "doitem", "undoitem", "redoitem", "abortheory",
     "retracttheory", "loadfile", "openfile", "closefile",
     "abortfile", "changecwd", "systemcmd"];

fun usespgip () =
    issue_pgip
        "usespgip"
        [("version", isabelle_pgip_version_supported)]
        (XML.element "acceptedpgipelems" []
                     (map (fn s=>XML.element "pgipelem"
                                             [] (* if threads: possibility to add async here *)
                                             [s])
                          isabelle_acceptedpgipelems))

fun usespgml () =
    issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)]

fun hasprefs () =
    List.app (fn (prefcat, prefs) =>
            issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
                 (map (fn (name, (descr, (ty, (default,_),_))) =>
                       XML.element "haspref" [("name", name),
                                              ("descr", descr),
                                              ("default", default)]
                       [ty]) prefs)]) (!preferences)

fun allprefs () = Library.foldl (op @) ([], map snd (!preferences))

fun setpref name value =
    (case AList.lookup (op =) (allprefs ()) name of
         NONE => warning ("Unknown pref: " ^ quote name)
       | SOME (_, (_, _, set)) => set value);

fun getpref name =
    (case AList.lookup (op =) (allprefs ()) name of
         NONE => warning ("Unknown pref: " ^ quote name)
       | SOME (_, (_, (_,get), _)) =>
           issue_pgip "prefval" [("name", name)] (get ()));



(**** PGIP:  Interface -> Isabelle/Isar ****)

exception PGIP of string;
exception PGIP_QUIT;


(* Sending commands to Isar *)

fun isarcmd s =
    s |> OuterSyntax.scan |> OuterSyntax.read
      |> map (Toplevel.position (Position.name "PGIP message") o #3) |> Toplevel.>>>;

fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts)
  | xmltext [] = ""
  | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"

fun isarscript xmls = isarcmd (xmltext xmls)   (* send a script command *)


(* load an arbitrary file (must be .thy or .ML) *)

fun use_thy_or_ml_file file =
    let
        val (path,extn) = Path.split_ext (Path.unpack file)
    in
        case extn of
            "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
          | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
          | "ML" => isarcmd ("use " ^ quote file)
          | other => error ("Don't know how to read a file with extension " ^ other)
    end


(* Proof control commands *)

local
  fun xmlattro attr attrs = AList.lookup (op =) attrs attr

  fun xmlattr attr attrs =
      (case xmlattro attr attrs of
           SOME value => value
         | NONE => raise PGIP ("Missing attribute: " ^ attr))

  val thyname_attro = xmlattro "thyname"
  val thyname_attr = xmlattr "thyname"
  val objtype_attro = xmlattro "objtype"
  val objtype_attr = xmlattr "objtype"
  val name_attr = xmlattr "name"
  val dirname_attr = xmlattr "dir"
  fun comment x = "(* " ^ x ^ " *)"

  fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
      case Url.unpack url of
          (Url.File path) => File.platform_path path
        | _ => error ("Cannot access non-local URL " ^ url)

  val fileurl_of = localfile_of_url o (xmlattr "url")

  val topthy = Toplevel.theory_of o Toplevel.get_state
  val topthy_name = Context.theory_name o topthy

  val currently_open_file = ref (NONE : string option)

  (* Path management: we allow theory files to have dependencies
     in their own directory, but when we change directory for a new
     file we remove the path.  Leaving it there can cause confusion
     with difference in batch mode.a  NB: PGIP does not assume
     that the prover has a load path. *)
  local
      val current_working_dir = ref (NONE : string option)
  in
      fun changecwd dir =
          (case (!current_working_dir) of
               NONE => ()
             | SOME dir => ThyLoad.del_path dir;
           ThyLoad.add_path dir;
           current_working_dir := SOME dir)
  end

  val topnode = Toplevel.node_of o Toplevel.get_state
  fun topproofpos () = (case topnode() of Toplevel.Proof ph => SOME(ProofHistory.position ph)
                                        | _ => NONE) handle Toplevel.UNDEF => NONE
in

fun process_pgip_element pgipxml = (case pgipxml of
  (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
| (xml as (XML.Elem (elem, attrs, data))) =>
  (case elem of
       (* protocol config *)
       "askpgip"        => (pgip_emacs_compatibility_flag:=false; (* PG>=3.6 or other PGIP interface *)
                            usespgip (); send_pgip_config ())
     | "askpgml"        => usespgml ()
     (* proverconfig *)
     | "askprefs"       => hasprefs ()
     | "getpref"        => getpref (name_attr attrs)
     | "setpref"        => setpref (name_attr attrs) (xmltext data)
     (* provercontrol *)
     | "proverinit"     => isar_restart ()
     | "proverexit"     => isarcmd "quit"
     | "startquiet"     => isarcmd "disable_pr"
     | "stopquiet"      => isarcmd "enable_pr"
     | "pgmlsymbolson"   => change print_mode (insert (op =) Symbol.xsymbolsN)
     | "pgmlsymbolsoff"  => change print_mode (remove (op =) Symbol.xsymbolsN)
     (* properproofcmd: proper commands which belong in script *)
     (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
     (* NB: Isar doesn't make lemma name of goal accessible during proof *)
     | "opengoal"       => isarscript data
     | "proofstep"      => isarscript data
     | "closegoal"      => isarscript data
     | "giveupgoal"     => isarscript data
     | "postponegoal"   => isarscript data
     | "comment"        => isarscript data  (* NB: should be ignored, but process anyway *)
     | "whitespace"     => isarscript data  (* NB: should be ignored, but process anyway *)
     | "litcomment"     => isarscript data
     | "spuriouscmd"    => isarscript data
     | "badcmd"         => isarscript data
     (* improperproofcmd: improper commands which *do not* belong in script *)
     | "dostep"         => isarscript data
     | "undostep"       => isarcmd "undos_proof 1"
     | "redostep"       => isarcmd "redo"
     | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"
     | "forget"         => error "Not implemented"
     | "restoregoal"    => error "Not implemented"  (* could just treat as forget? *)
     (* proofctxt: improper commands *)
     | "askids"         => askids (thyname_attro attrs, objtype_attro attrs)
     | "showid"         => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
     | "askguise"       => send_informguise (!currently_open_file,
                                             SOME (topthy_name()) handle Toplevel.UNDEF => NONE,
                                             topproofpos())
     | "parsescript"    => parsescript (xmltext data) attrs (* just pass back attrs unchanged *)
     | "showproofstate" => isarcmd "pr"
     | "showctxt"       => isarcmd "print_theory"   (* more useful than print_context *)
     | "searchtheorems" => isarcmd ("thms_containing " ^ xmltext data)
     | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ xmltext data)
     | "viewdoc"        => isarcmd ("print_" ^ xmltext data) (* FIXME: isatool doc? *)
     (* properfilecmd: proper theory-level script commands *)
     (* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *)
     | "opentheory"     => isarscript data
     | "theoryitem"     => isarscript data
     | "closetheory"    => let
                              val thyname = topthy_name()
                           in (isarscript data;
                               writeln ("Theory " ^ quote thyname ^ " completed."))
                           end
     (* improperfilecmd: theory-level commands not in script *)
     | "doitem"         => isarscript data
     | "undoitem"       => isarcmd "ProofGeneral.undo"
     | "redoitem"       => isarcmd "ProofGeneral.redo"
     | "aborttheory"    => isarcmd ("init_toplevel")
     | "retracttheory"  => isarcmd ("kill_thy " ^ quote (thyname_attr attrs))
     | "loadfile"       => use_thy_or_ml_file (fileurl_of attrs)
     | "openfile"       => (openfile_retract (fileurl_of attrs);
                            currently_open_file := SOME (fileurl_of attrs))
     | "closefile"      => (case !currently_open_file of
                                SOME f => (inform_file_processed f;
                                           currently_open_file := NONE)
                              | NONE => raise PGIP ("closefile when no file is open!"))
     | "abortfile"      => (currently_open_file := NONE) (* perhaps error for no file open *)
     | "changecwd"      => changecwd (dirname_attr attrs)
     | "systemcmd"      => isarscript data
     (* unofficial command for debugging *)
     | "quitpgip" => raise PGIP_QUIT
     | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))

fun process_pgip_tree xml =
    (pgip_refid := NONE;
     pgip_refseq := NONE;
     (case xml of
          XML.Elem ("pgip", attrs, pgips) =>
          (let
               val class = xmlattr "class" attrs
               val dest  = xmlattro "destid" attrs
               val _ = (pgip_refid :=  xmlattro "id" attrs;
                        pgip_refseq := xmlattro "seq" attrs)
           in
               (* We respond to broadcast messages to provers, or
                  messages intended uniquely for us.  Silently ignore rest. *)
               case dest of
                   NONE => if (class = "pa") then
                               (List.app process_pgip_element pgips; true)
                           else false
                 | SOME id => if (matching_pgip_id id) then
                                  (List.app process_pgip_element pgips; true)
                              else false
           end)
        | _ => raise PGIP "Invalid PGIP packet received")
     handle (PGIP msg) =>
            (error (msg ^ "\nPGIP error occured in XML text below:\n" ^
                    (XML.string_of_tree xml))))

val process_pgip = K () o process_pgip_tree o XML.tree_of_string

end


(* PGIP loop: process PGIP input only *)

local

exception XML_PARSE

fun loop ready src =
    let
        val _ = if ready then (issue_pgipe "ready" []) else ()
        val pgipo = (Source.get_single src)
                        handle e => raise XML_PARSE
    in
        case pgipo of
             NONE  => ()
           | SOME (pgip,src') =>
             let
                 val ready' = (process_pgip_tree pgip) handle e => (handler (e,SOME src'); true)
             in
                 loop ready' src'
             end
    end handle e => handler (e,SOME src)  (* i.e. error in ready/XML parse *)

and handler (e,srco) =
    case (e,srco) of
        (XML_PARSE,SOME src) =>
        panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *)
      | (PGIP_QUIT,_) => ()
      | (ERROR,SOME src) => loop true src (* message already given *)
      | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src)
      | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *)
      | (e,SOME src) => (error (Toplevel.exn_message e); loop true src)
      | (_,NONE) => ()
in
  (* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *)

  val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single

  val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)

  fun pgip_toplevel x = loop true x
end


(* additional outer syntax for Isar *)

local structure P = OuterParse and K = OuterKeyword in

val undoP = (*undo without output*)
  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));

val redoP = (*redo without output*)
  OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
    (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));

val context_thy_onlyP =
  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
    (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));

val try_context_thy_onlyP =
  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
    (P.name >> (Toplevel.no_timing oo
      (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));

val restartP =
  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));

val kill_proofP =
  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));

val inform_file_processedP =
  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
    (P.name >> (fn file => Toplevel.no_timing o
      Toplevel.keep (vacuous_inform_file_processed file) o
      Toplevel.kill o
      Toplevel.keep (proper_inform_file_processed file)));

val inform_file_retractedP =
  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
    (P.name >> (Toplevel.no_timing oo
      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));

val process_pgipP =
  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
    (P.text >> (Toplevel.no_timing oo
      (fn txt => Toplevel.imperative (fn () => process_pgip txt))));

fun init_outer_syntax () = OuterSyntax.add_parsers
 [undoP, redoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
  inform_file_processedP, inform_file_retractedP, process_pgipP];

end;


(* init *)

val initialized = ref false;

fun set_prompts true _ = ml_prompts "ML> " "ML# "
  | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
  | set_prompts false false = ml_prompts ("> " ^ special "372") ("- " ^ special "373");

fun init_setup isar pgip =
  (conditional (not (! initialized)) (fn () =>
   (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
    setup_xsymbols_output ();
    setup_pgml_output ();
    setup_messages ();
    setup_state ();
    setup_thy_loader ();
    setup_present_hook ();
    set initialized; ()));
  sync_thy_loader ();
  change print_mode (cons proof_generalN o remove (op =) proof_generalN);
  if pgip then
      (init_pgip_session_id();
       change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN]))
  else
    pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
  set quick_and_dirty;
  ThmDeps.enable ();
  set_prompts isar pgip;
  pgip_active := pgip);

fun init isar =
 (init_setup isar false;
  if isar then Isar.sync_main () else isa_restart ());

fun init_pgip false = panic "PGIP not supported for Isabelle/classic mode."
  | init_pgip true = (init_setup true true; pgip_toplevel tty_src);



(** generate elisp file for keyword classification **)

local

val regexp_meta = explode ".*+?[]^$";
val regexp_quote =
  implode o map (fn c => if c mem_string regexp_meta then "\\\\" ^ c else c) o explode;

fun defconst name strs =
  "\n(defconst isar-keywords-" ^ name ^
  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";

fun make_elisp_commands commands kind = defconst kind
  (commands |> List.mapPartial (fn (c, _, k, _) => if k = kind then SOME c else NONE));

fun make_elisp_syntax (keywords, commands) =
  ";;\n\
  \;; Keyword classification tables for Isabelle/Isar.\n\
  \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
  \;;\n\
  \;; $" ^ "Id$\n\
  \;;\n" ^
  defconst "major" (map #1 commands) ^
  defconst "minor" (List.filter Syntax.is_identifier keywords) ^
  implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
  "\n(provide 'isar-keywords)\n";

in

fun write_keywords s =
 (init_outer_syntax ();
  File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
    (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));

end;

end;