src/Pure/ProofGeneral/proof_general_emacs.ML
author wenzelm
Fri Dec 29 19:50:50 2006 +0100 (2006-12-29)
changeset 21948 e34bc5e4e7bc
parent 21945 4dd9a5fc7fc3
child 21959 b50182aff75f
permissions -rw-r--r--
removed obsolete init_pgip;
removed obsolete redo, context_thy etc.;
     1 (*  Title:      Pure/ProofGeneral/proof_general_emacs.ML
     2     ID:         $Id$
     3     Author:     David Aspinall and Markus Wenzel
     4 
     5 Isabelle/Isar configuration for Emacs Proof General.
     6 See http://proofgeneral.inf.ed.ac.uk
     7 *)
     8 
     9 signature PROOF_GENERAL =
    10 sig
    11   val init: bool -> unit
    12   val write_keywords: string -> unit
    13 end;
    14 
    15 structure ProofGeneral: PROOF_GENERAL =
    16 struct
    17 
    18 structure P = OuterParse;
    19 
    20 
    21 (* print modes *)
    22 
    23 val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
    24 val pgasciiN = "PGASCII";                  (*plain 7-bit ASCII communication*)
    25 val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
    26 
    27 fun special oct =
    28   if Output.has_mode pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
    29   else oct_char oct;
    30 
    31 
    32 (* text output: print modes for xsymbol *)
    33 
    34 local
    35 
    36 fun xsym_output "\\" = "\\\\"
    37   | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
    38 
    39 fun xsymbols_output s =
    40   if Output.has_mode Symbol.xsymbolsN andalso exists_string (equal "\\") s then
    41     let val syms = Symbol.explode s
    42     in (implode (map xsym_output syms), real (Symbol.length syms)) end
    43   else Symbol.default_output s;
    44 
    45 in
    46 
    47 fun setup_xsymbols_output () =
    48   Output.add_mode Symbol.xsymbolsN
    49     (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
    50 
    51 end;
    52 
    53 
    54 (* token translations *)
    55 
    56 local
    57 
    58 fun end_tag () = special "350";
    59 val class_tag = ("class", fn () => special "351");
    60 val tfree_tag = ("tfree", fn () => special "352");
    61 val tvar_tag = ("tvar", fn () => special "353");
    62 val free_tag = ("free", fn () => special "354");
    63 val bound_tag = ("bound", fn () => special "355");
    64 val var_tag = ("var", fn () => special "356");
    65 val skolem_tag = ("skolem", fn () => special "357");
    66 
    67 fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
    68 
    69 fun tagit (kind, bg_tag) x =
    70   (bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
    71 
    72 fun free_or_skolem x =
    73   (case try Name.dest_skolem x of
    74     NONE => tagit free_tag x
    75   | SOME x' => tagit skolem_tag x');
    76 
    77 fun var_or_skolem s =
    78   (case Syntax.read_variable s of
    79     SOME (x, i) =>
    80       (case try Name.dest_skolem x of
    81         NONE => tagit var_tag s
    82       | SOME x' => tagit skolem_tag
    83           (setmp show_question_marks true Syntax.string_of_vname (x', i)))
    84   | NONE => tagit var_tag s);
    85 
    86 val proof_general_trans =
    87  Syntax.tokentrans_mode proof_generalN
    88   [("class", tagit class_tag),
    89    ("tfree", tagit tfree_tag),
    90    ("tvar", tagit tvar_tag),
    91    ("free", free_or_skolem),
    92    ("bound", tagit bound_tag),
    93    ("var", var_or_skolem)];
    94 
    95 in
    96 
    97 val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
    98 
    99 end;
   100 
   101 
   102 (* messages and notification *)
   103 
   104 fun decorate bg en prfx =
   105   writeln_default o enclose bg en o prefix_lines prfx;
   106 
   107 fun setup_messages () =
   108  (writeln_fn := (fn s => decorate "" "" "" s);
   109   priority_fn := (fn s => decorate (special "360") (special "361") "" s);
   110   tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
   111   info_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
   112   debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
   113   warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
   114   error_fn := (fn s => decorate (special "364") (special "365") "*** " s);
   115   panic_fn := (fn s => decorate (special "364") (special "365") "!!! " s));
   116 
   117 
   118 fun emacs_notify s = decorate (special "360") (special "361") "" s;
   119 
   120 fun tell_clear_goals () =
   121   emacs_notify "Proof General, please clear the goals buffer.";
   122 
   123 fun tell_clear_response () =
   124   emacs_notify "Proof General, please clear the response buffer.";
   125 
   126 fun tell_file_loaded path =
   127   emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
   128 
   129 fun tell_file_retracted path =
   130   emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
   131 
   132 
   133 (* theory / proof state output *)
   134 
   135 local
   136 
   137 fun tmp_markers f =
   138   setmp Display.current_goals_markers (special "366", special "367", "") f ();
   139 
   140 fun print_current_goals n m st =
   141   tmp_markers (fn () => Display.print_current_goals_default n m st);
   142 
   143 fun print_state b st =
   144   tmp_markers (fn () => Toplevel.print_state_default b st);
   145 
   146 in
   147 
   148 fun setup_state () =
   149  (Display.print_current_goals_fn := print_current_goals;
   150   Toplevel.print_state_fn := print_state;
   151   Toplevel.prompt_state_fn :=
   152     (fn s => suffix (special "372") (Toplevel.prompt_state_default s)));
   153 
   154 end;
   155 
   156 
   157 (* theory loader actions *)
   158 
   159 local
   160 
   161 fun trace_action action name =
   162   if action = ThyInfo.Update then
   163     List.app tell_file_loaded (ThyInfo.loaded_files name)
   164   else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
   165     List.app tell_file_retracted (ThyInfo.loaded_files name)
   166   else ();
   167 
   168 in
   169   fun setup_thy_loader () = ThyInfo.add_hook trace_action;
   170   fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
   171 end;
   172 
   173 
   174 (* get informed about files *)
   175 
   176 val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
   177 
   178 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
   179 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
   180 val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
   181 
   182 fun proper_inform_file_processed file state =
   183   let val name = thy_name file in
   184     if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
   185      (ThyInfo.touch_child_thys name;
   186       ThyInfo.pretend_use_thy_only name handle ERROR msg =>
   187        (warning msg; warning ("Failed to register theory: " ^ quote name);
   188         tell_file_retracted (Path.base (Path.explode file))))
   189     else raise Toplevel.UNDEF
   190   end;
   191 
   192 fun vacuous_inform_file_processed file state =
   193  (warning ("No theory " ^ quote (thy_name file));
   194   tell_file_retracted (Path.base (Path.explode file)));
   195 
   196 
   197 (* restart top-level loop (keeps most state information) *)
   198 
   199 val welcome = priority o Session.welcome;
   200 
   201 fun restart () =
   202  (sync_thy_loader ();
   203   tell_clear_goals ();
   204   tell_clear_response ();
   205   welcome ();
   206   raise Toplevel.RESTART);
   207 
   208 
   209 (* theorem dependency output *)
   210 
   211 local
   212 
   213 val spaces_quote = space_implode " " o map quote;
   214 
   215 fun thm_deps_message (thms, deps) =
   216   emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
   217 
   218 (* FIXME: check this uses non-transitive closure function here *)
   219 fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
   220   let
   221     val names = filter_out (equal "") (map PureThy.get_name_hint ths);
   222     val deps = filter_out (equal "")
   223       (Symtab.keys (fold Proofterm.thms_of_proof
   224         (map Thm.proof_of ths) Symtab.empty));
   225   in
   226     if null names orelse null deps then ()
   227     else thm_deps_message (spaces_quote names, spaces_quote deps)
   228   end);
   229 
   230 in
   231 
   232 fun setup_present_hook () =
   233   Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
   234 
   235 end;
   236 
   237 
   238 (* additional outer syntax for Isar *)
   239 
   240 local structure P = OuterParse and K = OuterKeyword in
   241 
   242 val undoP = (*undo without output*)
   243   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
   244     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
   245 
   246 val restartP =
   247   OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
   248     (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
   249 
   250 val kill_proofP =
   251   OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
   252     (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
   253 
   254 val inform_file_processedP =
   255   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
   256     (P.name >> (fn file => Toplevel.no_timing o
   257       Toplevel.keep (vacuous_inform_file_processed file) o
   258       Toplevel.kill o
   259       Toplevel.keep (proper_inform_file_processed file)));
   260 
   261 val inform_file_retractedP =
   262   OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
   263     (P.name >> (Toplevel.no_timing oo
   264       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
   265 
   266 val process_pgipP =
   267   OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
   268     (P.text >> (Toplevel.no_timing oo
   269       (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
   270 
   271 fun init_outer_syntax () = OuterSyntax.add_parsers
   272  [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
   273 
   274 end;
   275 
   276 
   277 (* init *)
   278 
   279 val initialized = ref false;
   280 
   281 fun init false =
   282       Output.panic "Proof General support no longer available for Isabelle/classic mode."
   283   | init true =
   284       (conditional (not (! initialized)) (fn () =>
   285        (setmp warning_fn (K ()) init_outer_syntax ();
   286         setup_xsymbols_output ();
   287         setup_messages ();
   288         ProofGeneralPgip.init_pgip_channel (! priority_fn);
   289         setup_state ();
   290         setup_thy_loader ();
   291         setup_present_hook ();
   292         set initialized; ()));
   293       sync_thy_loader ();
   294       change print_mode (cons proof_generalN o remove (op =) proof_generalN);
   295       ml_prompts "ML> " "ML# ";
   296       Isar.sync_main ());
   297 
   298 
   299 
   300 (** generate elisp file for keyword classification **)
   301 
   302 local
   303 
   304 val regexp_meta = member (op =) (explode ".*+?[]^$");
   305 val regexp_quote = translate_string (fn c => if regexp_meta c then "\\\\" ^ c else c);
   306 
   307 fun defconst name strs =
   308   "\n(defconst isar-keywords-" ^ name ^
   309   "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
   310 
   311 fun make_elisp_commands commands kind = defconst kind
   312   (commands |> map_filter (fn (c, _, k, _) => if k = kind then SOME c else NONE));
   313 
   314 fun make_elisp_syntax (keywords, commands) =
   315   ";;\n\
   316   \;; Keyword classification tables for Isabelle/Isar.\n\
   317   \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
   318   \;;\n\
   319   \;; $" ^ "Id$\n\
   320   \;;\n" ^
   321   defconst "major" (map #1 commands) ^
   322   defconst "minor" (filter Syntax.is_identifier keywords) ^
   323   implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
   324   "\n(provide 'isar-keywords)\n";
   325 
   326 in
   327 
   328 fun write_keywords s =
   329  (init_outer_syntax ();
   330   File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
   331     (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
   332 
   333 end;
   334 
   335 end;