Add separate PG Emacs configuration
authoraspinall
Mon Dec 04 22:12:08 2006 +0100 (2006-12-04)
changeset 2164254b00ca67e0e
parent 21641 d73ab30e82dc
child 21643 bdf3e74727df
Add separate PG Emacs configuration
src/Pure/ProofGeneral/ROOT.ML
src/Pure/ProofGeneral/TODO
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/ROOT.ML	Mon Dec 04 22:11:28 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/ROOT.ML	Mon Dec 04 22:12:08 2006 +0100
     1.3 @@ -10,6 +10,4 @@
     1.4  use "parsing.ML";
     1.5  
     1.6  (use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general_pgip.ML";
     1.7 -(* OLD interaction mode, not yet complete
     1.8 -  (use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general_emacs.ML";
     1.9 -*)
    1.10 +(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general_emacs.ML";
     2.1 --- a/src/Pure/ProofGeneral/TODO	Mon Dec 04 22:11:28 2006 +0100
     2.2 +++ b/src/Pure/ProofGeneral/TODO	Mon Dec 04 22:12:08 2006 +0100
     2.3 @@ -1,7 +1,6 @@
     2.4  Major:
     2.5  
     2.6 - split out Emacs part of Pure/proof_general.ML and move here 
     2.7 - as proof_general_emacs.ML.  Remove isa support.
     2.8 + proof_general_emacs.ML fixups/PG compatibility: ongoing
     2.9  
    2.10   Complete pgip_types: add PGML and objtypes
    2.11  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Dec 04 22:12:08 2006 +0100
     3.3 @@ -0,0 +1,379 @@
     3.4 +(*  Title:      Pure/ProofGeneral/proof_general_emacs.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     David Aspinall and Markus Wenzel
     3.7 +
     3.8 +Isabelle/Isar configuration for Emacs Proof General.
     3.9 +See http://proofgeneral.inf.ed.ac.uk
    3.10 +*)
    3.11 +
    3.12 +signature PROOF_GENERAL =
    3.13 +sig
    3.14 +  val init: bool -> unit
    3.15 +  val init_pgip: bool -> unit	        (* for compatibility; always fails *)
    3.16 +  val write_keywords: string -> unit
    3.17 +end;
    3.18 +
    3.19 +structure ProofGeneral: PROOF_GENERAL =
    3.20 +struct
    3.21 +
    3.22 +structure P = OuterParse;
    3.23 +
    3.24 +(* print modes *)
    3.25 +
    3.26 +val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
    3.27 +val pgasciiN = "PGASCII";                  (*plain 7-bit ASCII communication*)
    3.28 +val xsymbolsN = Symbol.xsymbolsN;          (*X-Symbol symbols*)
    3.29 +val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
    3.30 +
    3.31 +fun special oct =
    3.32 +  if Output.has_mode pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
    3.33 +  else oct_char oct;
    3.34 +
    3.35 +
    3.36 +(* text output: print modes for xsymbol *)
    3.37 +
    3.38 +local
    3.39 +
    3.40 +fun xsym_output "\\" = "\\\\"
    3.41 +  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
    3.42 +
    3.43 +fun xsymbols_output s =
    3.44 +  if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then
    3.45 +    let val syms = Symbol.explode s
    3.46 +    in (implode (map xsym_output syms), real (Symbol.length syms)) end
    3.47 +  else Symbol.default_output s;
    3.48 +
    3.49 +in
    3.50 +
    3.51 +fun setup_xsymbols_output () =
    3.52 +  Output.add_mode xsymbolsN
    3.53 +    (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
    3.54 +
    3.55 +end;
    3.56 +
    3.57 +
    3.58 +(* token translations *)
    3.59 +
    3.60 +local
    3.61 +
    3.62 +fun end_tag () = special "350";
    3.63 +val class_tag = ("class", fn () => special "351");
    3.64 +val tfree_tag = ("tfree", fn () => special "352");
    3.65 +val tvar_tag = ("tvar", fn () => special "353");
    3.66 +val free_tag = ("free", fn () => special "354");
    3.67 +val bound_tag = ("bound", fn () => special "355");
    3.68 +val var_tag = ("var", fn () => special "356");
    3.69 +val skolem_tag = ("skolem", fn () => special "357");
    3.70 +
    3.71 +fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
    3.72 +
    3.73 +fun tagit (kind, bg_tag) x =
    3.74 +    (bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
    3.75 +
    3.76 +fun free_or_skolem x =
    3.77 +  (case try Name.dest_skolem x of
    3.78 +    NONE => tagit free_tag x
    3.79 +  | SOME x' => tagit skolem_tag x');
    3.80 +
    3.81 +fun var_or_skolem s =
    3.82 +  (case Syntax.read_variable s of
    3.83 +    SOME (x, i) =>
    3.84 +      (case try Name.dest_skolem x of
    3.85 +        NONE => tagit var_tag s
    3.86 +      | SOME x' => tagit skolem_tag
    3.87 +          (setmp show_question_marks true Syntax.string_of_vname (x', i)))
    3.88 +  | NONE => tagit var_tag s);
    3.89 +
    3.90 +val proof_general_trans =
    3.91 + Syntax.tokentrans_mode proof_generalN
    3.92 +  [("class", tagit class_tag),
    3.93 +   ("tfree", tagit tfree_tag),
    3.94 +   ("tvar", tagit tvar_tag),
    3.95 +   ("free", free_or_skolem),
    3.96 +   ("bound", tagit bound_tag),
    3.97 +   ("var", var_or_skolem)];
    3.98 +
    3.99 +in
   3.100 +
   3.101 +val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
   3.102 +
   3.103 +end;
   3.104 +
   3.105 +
   3.106 +(* messages and notification *)
   3.107 +
   3.108 +fun decorate bg en prfx =
   3.109 +  writeln_default o enclose bg en o prefix_lines prfx;
   3.110 +
   3.111 +fun setup_messages () =
   3.112 + (writeln_fn := (fn s => decorate "" "" "" s);
   3.113 +  priority_fn := (fn s => decorate (special "360") (special "361") "" s);
   3.114 +  tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
   3.115 +  info_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
   3.116 +  debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
   3.117 +  warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
   3.118 +  error_fn := (fn s => decorate (special "364") (special "365") "*** " s);
   3.119 +  panic_fn := (fn s => decorate (special "364") (special "365") "!!! " s));
   3.120 +
   3.121 +
   3.122 +fun emacs_notify s = decorate (special "360") (special "361") "" s;
   3.123 +
   3.124 +fun tell_clear_goals () =
   3.125 +    emacs_notify "Proof General, please clear the goals buffer.";
   3.126 +
   3.127 +fun tell_clear_response () =
   3.128 +    emacs_notify "Proof General, please clear the response buffer.";
   3.129 +
   3.130 +fun tell_file_loaded path =
   3.131 +    emacs_notify ("Proof General, this file is loaded: " ^ 
   3.132 +		  quote (File.platform_path path));
   3.133 +
   3.134 +fun tell_file_retracted path =
   3.135 +    emacs_notify ("Proof General, you can unlock the file " 
   3.136 +		  ^ quote (File.platform_path path));
   3.137 +
   3.138 +
   3.139 +(* theory / proof state output *)
   3.140 +
   3.141 +local
   3.142 +
   3.143 +fun tmp_markers f =
   3.144 +  setmp Display.current_goals_markers (special "366", special "367", "") f ();
   3.145 +
   3.146 +fun print_current_goals n m st =
   3.147 +    tmp_markers (fn () => Display.print_current_goals_default n m st);
   3.148 +
   3.149 +fun print_state b st =
   3.150 +    tmp_markers (fn () => Toplevel.print_state_default b st);
   3.151 +
   3.152 +in
   3.153 +
   3.154 +fun setup_state () =
   3.155 +  (Display.print_current_goals_fn := print_current_goals;
   3.156 +   Toplevel.print_state_fn := print_state;
   3.157 +   Toplevel.prompt_state_fn := (fn s => suffix (special "372")
   3.158 +     (Toplevel.prompt_state_default s)));
   3.159 +
   3.160 +end;
   3.161 +
   3.162 +
   3.163 +(* theory loader actions *)
   3.164 +
   3.165 +local
   3.166 +
   3.167 +fun trace_action action name =
   3.168 +  if action = ThyInfo.Update then
   3.169 +    List.app tell_file_loaded (ThyInfo.loaded_files name)
   3.170 +  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
   3.171 +    List.app tell_file_retracted (ThyInfo.loaded_files name)
   3.172 +  else ();
   3.173 +
   3.174 +in
   3.175 +  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
   3.176 +  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
   3.177 +end;
   3.178 +
   3.179 +
   3.180 +(* prepare theory context *)
   3.181 +
   3.182 +val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
   3.183 +
   3.184 +(* FIXME general treatment of tracing*)
   3.185 +val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
   3.186 +
   3.187 +fun dynamic_context () =
   3.188 +  (case Context.get_context () of
   3.189 +    SOME thy => "  Using current (dynamic!) one: " ^ quote (Context.theory_name thy)
   3.190 +  | NONE => "");
   3.191 +
   3.192 +fun try_update_thy_only file =
   3.193 +  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
   3.194 +    let val name = thy_name file in
   3.195 +      if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
   3.196 +      then update_thy_only name
   3.197 +      else warning ("Unkown theory context of ML file." ^ dynamic_context ())
   3.198 +    end) ();
   3.199 +
   3.200 +
   3.201 +(* get informed about files *)
   3.202 +
   3.203 +val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
   3.204 +val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
   3.205 +val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
   3.206 +
   3.207 +fun proper_inform_file_processed file state =
   3.208 +  let val name = thy_name file in
   3.209 +    if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
   3.210 +     (ThyInfo.touch_child_thys name;
   3.211 +      ThyInfo.pretend_use_thy_only name handle ERROR msg =>
   3.212 +       (warning msg; warning ("Failed to register theory: " ^ quote name);
   3.213 +        tell_file_retracted (Path.base (Path.unpack file))))
   3.214 +    else raise Toplevel.UNDEF
   3.215 +  end;
   3.216 +
   3.217 +fun vacuous_inform_file_processed file state =
   3.218 + (warning ("No theory " ^ quote (thy_name file));
   3.219 +  tell_file_retracted (Path.base (Path.unpack file)));
   3.220 +
   3.221 +
   3.222 +(* restart top-level loop (keeps most state information) *)
   3.223 +
   3.224 +val welcome = priority o Session.welcome;
   3.225 +
   3.226 +fun restart () =
   3.227 +    (sync_thy_loader ();
   3.228 +     tell_clear_goals ();
   3.229 +     tell_clear_response ();
   3.230 +     welcome ();
   3.231 +     raise Toplevel.RESTART)
   3.232 +
   3.233 +
   3.234 +(* theorem dependency output *)
   3.235 +
   3.236 +local
   3.237 +
   3.238 +val spaces_quote = space_implode " " o map quote;
   3.239 +
   3.240 +fun thm_deps_message (thms, deps) =
   3.241 +    emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
   3.242 +
   3.243 +(* FIXME: check this uses non-transitive closure function here *)
   3.244 +fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
   3.245 +  let
   3.246 +    val names = filter_out (equal "") (map Thm.name_of_thm ths);
   3.247 +    val deps = filter_out (equal "")
   3.248 +      (Symtab.keys (fold Proofterm.thms_of_proof
   3.249 +        (map Thm.proof_of ths) Symtab.empty));
   3.250 +  in
   3.251 +    if null names orelse null deps then ()
   3.252 +    else thm_deps_message (spaces_quote names, spaces_quote deps)
   3.253 +  end);
   3.254 +
   3.255 +in
   3.256 +
   3.257 +fun setup_present_hook () =
   3.258 +  Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
   3.259 +
   3.260 +end;
   3.261 +
   3.262 +
   3.263 +(* additional outer syntax for Isar *)
   3.264 +
   3.265 +local structure P = OuterParse and K = OuterKeyword in
   3.266 +
   3.267 +val undoP = (*undo without output*)
   3.268 +  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
   3.269 +    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
   3.270 +
   3.271 +val redoP = (*redo without output*)
   3.272 +  OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
   3.273 +    (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
   3.274 +
   3.275 +val context_thy_onlyP =
   3.276 +  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
   3.277 +    (P.name >> (Toplevel.no_timing oo IsarCmd.init_context update_thy_only));
   3.278 +
   3.279 +val try_context_thy_onlyP =
   3.280 +  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
   3.281 +    (P.name >> (Toplevel.no_timing oo
   3.282 +      (Toplevel.imperative (K ()) oo IsarCmd.init_context try_update_thy_only)));
   3.283 +
   3.284 +val restartP =
   3.285 +  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
   3.286 +    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
   3.287 +
   3.288 +val kill_proofP =
   3.289 +  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
   3.290 +    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
   3.291 +
   3.292 +val inform_file_processedP =
   3.293 +  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
   3.294 +    (P.name >> (fn file => Toplevel.no_timing o
   3.295 +      Toplevel.keep (vacuous_inform_file_processed file) o
   3.296 +      Toplevel.kill o
   3.297 +      Toplevel.keep (proper_inform_file_processed file)));
   3.298 +
   3.299 +val inform_file_retractedP =
   3.300 +  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
   3.301 +    (P.name >> (Toplevel.no_timing oo
   3.302 +      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
   3.303 +
   3.304 +val process_pgipP =
   3.305 +  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
   3.306 +    (P.text >> (Toplevel.no_timing oo
   3.307 +      (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
   3.308 +
   3.309 +fun init_outer_syntax () = OuterSyntax.add_parsers
   3.310 + [undoP, redoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
   3.311 +  inform_file_processedP, inform_file_retractedP, process_pgipP];
   3.312 +
   3.313 +end;
   3.314 +
   3.315 +
   3.316 +(* init *)
   3.317 +
   3.318 +val initialized = ref false;
   3.319 +
   3.320 +fun set_prompts () = ml_prompts "ML> " "ML# "
   3.321 +
   3.322 +fun init_setup () =
   3.323 +  (conditional (not (! initialized)) (fn () =>
   3.324 +   (setmp warning_fn (K ()) init_outer_syntax ();
   3.325 +    setup_xsymbols_output ();
   3.326 +    setup_messages ();
   3.327 +    setup_state ();
   3.328 +    setup_thy_loader ();
   3.329 +    setup_present_hook ();
   3.330 +    set initialized; ()));
   3.331 +  sync_thy_loader ();
   3.332 +  change print_mode (cons proof_generalN o remove (op =) proof_generalN);
   3.333 +  set_prompts ())
   3.334 +
   3.335 +fun init true = (init_setup ();
   3.336 +		 Isar.sync_main ())
   3.337 +  | init false = Output.panic "Interface support no longer available for Isabelle/classic mode."
   3.338 +
   3.339 +fun init_pgip false = init true
   3.340 +  | init_pgip true = Output.panic "No PGIP here, please use ProofGeneralPgip.init_pgip (update your isabelle-process script)."
   3.341 +
   3.342 +
   3.343 +
   3.344 +
   3.345 +(** generate elisp file for keyword classification **)
   3.346 +
   3.347 +local
   3.348 +
   3.349 +val regexp_meta = member (op =) (explode ".*+?[]^$");
   3.350 +val regexp_quote =
   3.351 +  implode o map (fn c => if regexp_meta c then "\\\\" ^ c else c) o explode;
   3.352 +
   3.353 +fun defconst name strs =
   3.354 +  "\n(defconst isar-keywords-" ^ name ^
   3.355 +  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
   3.356 +
   3.357 +fun make_elisp_commands commands kind = defconst kind
   3.358 +  (commands |> map_filter (fn (c, _, k, _) => if k = kind then SOME c else NONE));
   3.359 +
   3.360 +fun make_elisp_syntax (keywords, commands) =
   3.361 +  ";;\n\
   3.362 +  \;; Keyword classification tables for Isabelle/Isar.\n\
   3.363 +  \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
   3.364 +  \;;\n\
   3.365 +  \;; $" ^ "Id$\n\
   3.366 +  \;;\n" ^
   3.367 +  defconst "major" (map #1 commands) ^
   3.368 +  defconst "minor" (List.filter Syntax.is_identifier keywords) ^
   3.369 +  implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
   3.370 +  "\n(provide 'isar-keywords)\n";
   3.371 +
   3.372 +in
   3.373 +
   3.374 +fun write_keywords s =
   3.375 + (init_outer_syntax ();
   3.376 +  File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
   3.377 +    (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
   3.378 +
   3.379 +end;
   3.380 +
   3.381 +
   3.382 +end;
     4.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Dec 04 22:11:28 2006 +0100
     4.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Dec 04 22:12:08 2006 +0100
     4.3 @@ -9,7 +9,10 @@
     4.4  
     4.5  signature PROOF_GENERAL_PGIP =
     4.6  sig
     4.7 -  val init_pgip: bool -> unit
     4.8 +  val init_pgip: bool -> unit		  (* main PGIP loop with true; fail with false *)
     4.9 +
    4.10 +  val process_pgip: string -> unit        (* process a command; only good for preferences *)
    4.11 +  val init_pgip_session_id: unit -> unit  (* call before using process_pgip *)
    4.12  end
    4.13  
    4.14  structure ProofGeneralPgip : PROOF_GENERAL_PGIP  =