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