aspinall@21642: (*  Title:      Pure/ProofGeneral/proof_general_emacs.ML
aspinall@21642:     ID:         $Id$
aspinall@21642:     Author:     David Aspinall and Markus Wenzel
aspinall@21642: 
aspinall@21642: Isabelle/Isar configuration for Emacs Proof General.
aspinall@21642: See http://proofgeneral.inf.ed.ac.uk
aspinall@21642: *)
aspinall@21642: 
aspinall@21642: signature PROOF_GENERAL =
aspinall@21642: sig
aspinall@21642:   val init: bool -> unit
wenzelm@24289:   val sendback: string -> Pretty.T list -> unit
aspinall@21642:   val write_keywords: string -> unit
aspinall@21642: end;
aspinall@21642: 
aspinall@21642: structure ProofGeneral: PROOF_GENERAL =
aspinall@21642: struct
aspinall@21642: 
wenzelm@21945: 
aspinall@21642: (* print modes *)
aspinall@21642: 
aspinall@21642: val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
aspinall@21642: val pgasciiN = "PGASCII";                  (*plain 7-bit ASCII communication*)
aspinall@21642: val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
aspinall@21642: 
aspinall@21642: fun special oct =
wenzelm@22590:   if print_mode_active pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
aspinall@21642:   else oct_char oct;
aspinall@21642: 
aspinall@21642: 
aspinall@21642: (* text output: print modes for xsymbol *)
aspinall@21642: 
aspinall@21642: local
aspinall@21642: 
aspinall@21642: fun xsym_output "\\" = "\\\\"
aspinall@21642:   | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
aspinall@21642: 
aspinall@21642: fun xsymbols_output s =
wenzelm@22590:   if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then
aspinall@21642:     let val syms = Symbol.explode s
wenzelm@23621:     in (implode (map xsym_output syms), Symbol.length syms) end
wenzelm@23621:   else Output.default_output s;
aspinall@21642: 
aspinall@21642: in
aspinall@21642: 
aspinall@21642: fun setup_xsymbols_output () =
wenzelm@23641:   Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
aspinall@21642: 
aspinall@21642: end;
aspinall@21642: 
aspinall@21642: 
aspinall@21642: (* token translations *)
aspinall@21642: 
aspinall@21642: local
aspinall@21642: 
aspinall@21642: fun end_tag () = special "350";
aspinall@21642: val class_tag = ("class", fn () => special "351");
aspinall@21642: val tfree_tag = ("tfree", fn () => special "352");
aspinall@21642: val tvar_tag = ("tvar", fn () => special "353");
aspinall@21642: val free_tag = ("free", fn () => special "354");
aspinall@21642: val bound_tag = ("bound", fn () => special "355");
aspinall@21642: val var_tag = ("var", fn () => special "356");
aspinall@21642: val skolem_tag = ("skolem", fn () => special "357");
aspinall@21642: 
aspinall@21642: fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
aspinall@21642: 
aspinall@21642: fun tagit (kind, bg_tag) x =
wenzelm@23621:   (bg_tag () ^ x ^ end_tag (), Symbol.length (Symbol.explode x));
aspinall@21642: 
aspinall@21642: fun free_or_skolem x =
aspinall@21642:   (case try Name.dest_skolem x of
aspinall@21642:     NONE => tagit free_tag x
aspinall@21642:   | SOME x' => tagit skolem_tag x');
aspinall@21642: 
aspinall@21642: fun var_or_skolem s =
wenzelm@24244:   (case Lexicon.read_variable s of
aspinall@21642:     SOME (x, i) =>
aspinall@21642:       (case try Name.dest_skolem x of
aspinall@21642:         NONE => tagit var_tag s
aspinall@21642:       | SOME x' => tagit skolem_tag
wenzelm@22678:           (setmp show_question_marks true Term.string_of_vname (x', i)))
aspinall@21642:   | NONE => tagit var_tag s);
aspinall@21642: 
aspinall@21642: val proof_general_trans =
aspinall@21642:  Syntax.tokentrans_mode proof_generalN
aspinall@21642:   [("class", tagit class_tag),
aspinall@21642:    ("tfree", tagit tfree_tag),
aspinall@21642:    ("tvar", tagit tvar_tag),
aspinall@21642:    ("free", free_or_skolem),
aspinall@21642:    ("bound", tagit bound_tag),
aspinall@21642:    ("var", var_or_skolem)];
aspinall@21642: 
aspinall@21642: in
aspinall@21642: 
wenzelm@24712: val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
aspinall@21642: 
aspinall@21642: end;
aspinall@21642: 
aspinall@21642: 
wenzelm@23641: (* common markup *)
wenzelm@23641: 
wenzelm@23641: fun proof_general_markup (name, props) =
wenzelm@23641:   (if name = Markup.promptN then ("", special "372")
wenzelm@23702:     else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
aspinall@24330:     else if name = Markup.sendbackN then (special "376", special "377")
wenzelm@24555:     else if name = Markup.hiliteN then (special "327", special "330")
wenzelm@23641:     else ("", ""))
wenzelm@23641:   |> (name <> Markup.promptN andalso print_mode_active "test_markup") ?
wenzelm@23641:     (fn (bg, en) =>
wenzelm@23641:       (bg ^ enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
wenzelm@23641:         enclose "</" ">" name ^ en));
wenzelm@23641: 
wenzelm@23702: val _ = Markup.add_mode proof_generalN proof_general_markup;
wenzelm@23641: 
wenzelm@23641: 
aspinall@21642: (* messages and notification *)
aspinall@21642: 
aspinall@21642: fun decorate bg en prfx =
wenzelm@22590:   Output.writeln_default o enclose bg en o prefix_lines prfx;
aspinall@21642: 
aspinall@21642: fun setup_messages () =
wenzelm@23662:  (Output.writeln_fn := Output.writeln_default;
wenzelm@22590:   Output.priority_fn := (fn s => decorate (special "360") (special "361") "" s);
wenzelm@22590:   Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
wenzelm@22590:   Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
wenzelm@22590:   Output.warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
wenzelm@22699:   Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s));
aspinall@21642: 
wenzelm@22699: fun panic s =
wenzelm@22699:   (decorate (special "364") (special "365") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
aspinall@21642: 
aspinall@21642: fun emacs_notify s = decorate (special "360") (special "361") "" s;
aspinall@21642: 
aspinall@21642: fun tell_clear_goals () =
wenzelm@21940:   emacs_notify "Proof General, please clear the goals buffer.";
aspinall@21642: 
aspinall@21642: fun tell_clear_response () =
wenzelm@21940:   emacs_notify "Proof General, please clear the response buffer.";
aspinall@21642: 
aspinall@21642: fun tell_file_loaded path =
wenzelm@21940:   emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
aspinall@21642: 
aspinall@21642: fun tell_file_retracted path =
wenzelm@21940:   emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
aspinall@21642: 
wenzelm@24289: fun sendback heading prts =
wenzelm@24289:   Pretty.writeln (Pretty.big_list heading [Pretty.markup Markup.sendback prts]);
wenzelm@24289: 
aspinall@21642: 
aspinall@21642: (* theory loader actions *)
aspinall@21642: 
aspinall@21642: local
aspinall@21642: 
aspinall@21642: fun trace_action action name =
aspinall@21642:   if action = ThyInfo.Update then
aspinall@21642:     List.app tell_file_loaded (ThyInfo.loaded_files name)
aspinall@21642:   else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
aspinall@21642:     List.app tell_file_retracted (ThyInfo.loaded_files name)
aspinall@21642:   else ();
aspinall@21642: 
aspinall@21642: in
aspinall@21642:   fun setup_thy_loader () = ThyInfo.add_hook trace_action;
aspinall@21642:   fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
aspinall@21642: end;
aspinall@21642: 
aspinall@21642: 
wenzelm@21948: (* get informed about files *)
aspinall@21642: 
wenzelm@21858: val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
aspinall@21642: 
aspinall@21642: val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
aspinall@21642: val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
aspinall@21642: 
wenzelm@23913: fun proper_inform_file_processed file () =
aspinall@21642:   let val name = thy_name file in
wenzelm@23913:     if ThyInfo.known_thy name then
aspinall@21642:      (ThyInfo.touch_child_thys name;
wenzelm@24079:       ThyInfo.register_thy name handle ERROR msg =>
wenzelm@23913:        (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
wenzelm@21858:         tell_file_retracted (Path.base (Path.explode file))))
aspinall@21642:     else raise Toplevel.UNDEF
aspinall@21642:   end;
aspinall@21642: 
wenzelm@23913: fun vacuous_inform_file_processed file () =
aspinall@21642:  (warning ("No theory " ^ quote (thy_name file));
wenzelm@21858:   tell_file_retracted (Path.base (Path.explode file)));
aspinall@21642: 
aspinall@21642: 
aspinall@21642: (* restart top-level loop (keeps most state information) *)
aspinall@21642: 
aspinall@21642: val welcome = priority o Session.welcome;
aspinall@21642: 
aspinall@21642: fun restart () =
wenzelm@21940:  (sync_thy_loader ();
wenzelm@21940:   tell_clear_goals ();
wenzelm@21940:   tell_clear_response ();
wenzelm@21940:   welcome ();
wenzelm@21940:   raise Toplevel.RESTART);
aspinall@21642: 
aspinall@21642: 
aspinall@21642: (* theorem dependency output *)
aspinall@21642: 
aspinall@21642: local
aspinall@21642: 
aspinall@21642: val spaces_quote = space_implode " " o map quote;
aspinall@21642: 
aspinall@21642: fun thm_deps_message (thms, deps) =
wenzelm@21948:   emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
aspinall@21642: 
wenzelm@21968: fun tell_thm_deps ths =
wenzelm@22590:   if print_mode_active thm_depsN then
wenzelm@21968:     let
wenzelm@22228:       val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
aspinall@22225:       val deps = Symtab.keys (fold Proofterm.thms_of_proof'
aspinall@22225: 				   (map Thm.proof_of ths) Symtab.empty);
wenzelm@21968:     in
wenzelm@21968:       if null names orelse null deps then ()
wenzelm@21968:       else thm_deps_message (spaces_quote names, spaces_quote deps)
wenzelm@21968:     end
wenzelm@21968:   else ();
aspinall@21642: 
aspinall@21642: in
aspinall@21642: 
aspinall@21642: fun setup_present_hook () =
aspinall@21642:   Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
aspinall@21642: 
aspinall@21642: end;
aspinall@21642: 
aspinall@21642: 
aspinall@21642: (* additional outer syntax for Isar *)
aspinall@21642: 
aspinall@21642: local structure P = OuterParse and K = OuterKeyword in
aspinall@21642: 
wenzelm@24867: fun undoP () = (*undo without output*)
aspinall@21642:   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
aspinall@21642:     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
aspinall@21642: 
wenzelm@24867: fun restartP () =
aspinall@21642:   OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
aspinall@21642:     (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
aspinall@21642: 
wenzelm@24867: fun kill_proofP () =
aspinall@21642:   OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
aspinall@21642:     (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
aspinall@21642: 
wenzelm@24867: fun inform_file_processedP () =
aspinall@21642:   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
aspinall@21642:     (P.name >> (fn file => Toplevel.no_timing o
wenzelm@21959:       Toplevel.init_empty (vacuous_inform_file_processed file) o
aspinall@21642:       Toplevel.kill o
wenzelm@21959:       Toplevel.init_empty (proper_inform_file_processed file)));
aspinall@21642: 
wenzelm@24867: fun inform_file_retractedP () =
aspinall@21642:   OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
aspinall@21642:     (P.name >> (Toplevel.no_timing oo
aspinall@21642:       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
aspinall@21642: 
wenzelm@24867: fun process_pgipP () =
aspinall@21642:   OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
aspinall@21642:     (P.text >> (Toplevel.no_timing oo
aspinall@21642:       (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
aspinall@21642: 
wenzelm@24867: fun init_outer_syntax () = List.app (fn f => f ())
wenzelm@21948:  [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
aspinall@21642: 
aspinall@21642: end;
aspinall@21642: 
aspinall@21642: 
aspinall@21642: (* init *)
aspinall@21642: 
aspinall@21642: val initialized = ref false;
aspinall@21642: 
wenzelm@22699: fun init false = panic "No Proof General interface support for Isabelle/classic mode."
wenzelm@21940:   | init true =
wenzelm@21968:       (! initialized orelse
wenzelm@22590:         (Output.no_warnings init_outer_syntax ();
wenzelm@21968:           setup_xsymbols_output ();
wenzelm@21968:           setup_messages ();
wenzelm@22590:           ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
wenzelm@21968:           setup_thy_loader ();
wenzelm@21968:           setup_present_hook ();
wenzelm@21968:           set initialized);
wenzelm@21968:         sync_thy_loader ();
wenzelm@21968:        change print_mode (cons proof_generalN o remove (op =) proof_generalN);
wenzelm@21968:        Isar.sync_main ());
aspinall@21642: 
aspinall@21642: 
aspinall@21642: 
wenzelm@21968:  (** generate elisp file for keyword classification **)
aspinall@21642: 
aspinall@21642: local
aspinall@21642: 
aspinall@21642: val regexp_meta = member (op =) (explode ".*+?[]^$");
wenzelm@21940: val regexp_quote = translate_string (fn c => if regexp_meta c then "\\\\" ^ c else c);
aspinall@21642: 
aspinall@21642: fun defconst name strs =
aspinall@21642:   "\n(defconst isar-keywords-" ^ name ^
aspinall@21642:   "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
aspinall@21642: 
aspinall@21642: fun make_elisp_commands commands kind = defconst kind
aspinall@21642:   (commands |> map_filter (fn (c, _, k, _) => if k = kind then SOME c else NONE));
aspinall@21642: 
aspinall@21642: fun make_elisp_syntax (keywords, commands) =
aspinall@21642:   ";;\n\
aspinall@21642:   \;; Keyword classification tables for Isabelle/Isar.\n\
aspinall@21642:   \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
aspinall@21642:   \;;\n\
aspinall@21642:   \;; $" ^ "Id$\n\
aspinall@21642:   \;;\n" ^
aspinall@21642:   defconst "major" (map #1 commands) ^
wenzelm@21940:   defconst "minor" (filter Syntax.is_identifier keywords) ^
aspinall@21642:   implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
aspinall@21642:   "\n(provide 'isar-keywords)\n";
aspinall@21642: 
aspinall@21642: in
aspinall@21642: 
aspinall@21642: fun write_keywords s =
aspinall@21642:  (init_outer_syntax ();
wenzelm@21858:   File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
aspinall@21642:     (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
aspinall@21642: 
aspinall@21642: end;
aspinall@21642: 
aspinall@21642: end;