moved files;
authorwenzelm
Wed May 15 20:34:42 2013 +0200 (2013-05-15)
changeset 520093b18ef9df768
parent 52008 bdb82afdcb92
child 52010 e91359bfc84a
moved files;
src/Pure/ProofGeneral/proof_general.ML
src/Pure/ProofGeneral/proof_general_pure.ML
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Tools/proof_general.ML
src/Pure/Tools/proof_general_pure.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general.ML	Wed May 15 20:28:43 2013 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,468 +0,0 @@
     1.4 -(*  Title:      Pure/ProofGeneral/proof_general.ML
     1.5 -    Author:     David Aspinall
     1.6 -    Author:     Makarius
     1.7 -
     1.8 -Isabelle/Isar configuration for Proof General / Emacs.
     1.9 -See also http://proofgeneral.inf.ed.ac.uk
    1.10 -*)
    1.11 -
    1.12 -signature PROOF_GENERAL =
    1.13 -sig
    1.14 -  type category = string
    1.15 -  val category_display: category
    1.16 -  val category_advanced_display: category
    1.17 -  val category_tracing: category
    1.18 -  val category_proof: category
    1.19 -  type pgiptype = string
    1.20 -  val pgipbool: pgiptype
    1.21 -  val pgipint: pgiptype
    1.22 -  val pgipfloat: pgiptype
    1.23 -  val pgipstring: pgiptype
    1.24 -  val preference_raw: category ->
    1.25 -    (unit -> string) -> (string -> unit) -> string -> string -> string -> unit
    1.26 -  val preference_bool: category -> bool Unsynchronized.ref -> string -> string -> unit
    1.27 -  val preference_int: category -> int Unsynchronized.ref -> string -> string -> unit
    1.28 -  val preference_real: category -> real Unsynchronized.ref -> string -> string -> unit
    1.29 -  val preference_string: category -> string Unsynchronized.ref -> string -> string -> unit
    1.30 -  val preference_option: category -> string -> string -> string -> unit
    1.31 -  structure ThyLoad: sig val add_path: string -> unit end
    1.32 -  val init: unit -> unit
    1.33 -  val thm_depsN: string
    1.34 -end;
    1.35 -
    1.36 -structure ProofGeneral: PROOF_GENERAL =
    1.37 -struct
    1.38 -
    1.39 -(** preferences **)
    1.40 -
    1.41 -(* type preference *)
    1.42 -
    1.43 -type category = string;
    1.44 -val category_display = "Display";
    1.45 -val category_advanced_display = "Advanced Display";
    1.46 -val category_tracing = "Tracing";
    1.47 -val category_proof = "Proof";
    1.48 -
    1.49 -type pgiptype = string;
    1.50 -val pgipbool = "pgipbool";
    1.51 -val pgipint = "pgipint";
    1.52 -val pgipfloat = "pgipint";  (*NB: PG 3.7.x and 4.0 lack pgipfloat, but accept floats as pgipint*)
    1.53 -val pgipstring = "pgipstring";
    1.54 -
    1.55 -type preference =
    1.56 - {name: string,
    1.57 -  descr: string,
    1.58 -  default: string,
    1.59 -  pgiptype: pgiptype,
    1.60 -  get: unit -> string,
    1.61 -  set: string -> unit};
    1.62 -
    1.63 -
    1.64 -(* global preferences *)
    1.65 -
    1.66 -local
    1.67 -  val preferences =
    1.68 -    Synchronized.var "ProofGeneral.preferences"
    1.69 -      ([(category_display, []),
    1.70 -        (category_advanced_display, []),
    1.71 -        (category_tracing, []),
    1.72 -        (category_proof, [])]: (category * preference list) list);
    1.73 -in
    1.74 -
    1.75 -fun add_preference category (pref: preference) =
    1.76 -  Synchronized.change preferences (map (fn (cat, prefs) =>
    1.77 -    if cat <> category then (cat, prefs)
    1.78 -    else
    1.79 -      if exists (fn {name, ...} => name = #name pref) prefs
    1.80 -      then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs))
    1.81 -      else (cat, prefs @ [pref])));
    1.82 -
    1.83 -fun get_preferences () = Synchronized.value preferences;
    1.84 -
    1.85 -end;
    1.86 -
    1.87 -fun set_preference name value =
    1.88 -  let val prefs = map (`(#name)) (maps snd (get_preferences ())) in
    1.89 -    (case AList.lookup (op =) prefs name of
    1.90 -      SOME {set, ...} => set value
    1.91 -    | NONE => error ("Unknown prover preference: " ^ quote name))
    1.92 -  end;
    1.93 -
    1.94 -
    1.95 -(* raw preferences *)
    1.96 -
    1.97 -fun preference_raw category raw_get raw_set typ name descr =
    1.98 -  let
    1.99 -    fun get () = CRITICAL raw_get;
   1.100 -    fun set x = CRITICAL (fn () => raw_set x);
   1.101 -    val pref = {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()};
   1.102 -  in add_preference category pref end;
   1.103 -
   1.104 -fun preference_ref category read write typ r =
   1.105 -  preference_raw category (fn () => read (! r)) (fn x => r := write x) typ;
   1.106 -
   1.107 -fun preference_bool category = preference_ref category Markup.print_bool Markup.parse_bool pgipbool;
   1.108 -fun preference_int category = preference_ref category Markup.print_int Markup.parse_int pgipint;
   1.109 -fun preference_real category = preference_ref category Markup.print_real Markup.parse_real pgipfloat;
   1.110 -fun preference_string category = preference_ref category I I pgipstring;
   1.111 -
   1.112 -
   1.113 -(* system options *)
   1.114 -
   1.115 -fun preference_option category option_name pgip_name descr =
   1.116 -  let
   1.117 -    val typ = Options.default_typ option_name;
   1.118 -    val pgiptype =
   1.119 -      if typ = Options.boolT then pgipbool
   1.120 -      else if typ = Options.intT then pgipint
   1.121 -      else if typ = Options.realT then pgipfloat
   1.122 -      else pgipstring;
   1.123 -  in
   1.124 -    add_preference category
   1.125 -     {name = pgip_name,
   1.126 -      descr = descr,
   1.127 -      default = Options.get_default option_name,
   1.128 -      pgiptype = pgiptype,
   1.129 -      get = fn () => Options.get_default option_name,
   1.130 -      set = Options.put_default option_name}
   1.131 -  end;
   1.132 -
   1.133 -
   1.134 -(* minimal PGIP support for <askprefs>, <haspref>, <setpref> *)
   1.135 -
   1.136 -local
   1.137 -
   1.138 -fun get_attr attrs name =
   1.139 -  (case Properties.get attrs name of
   1.140 -    SOME value => value
   1.141 -  | NONE => raise Fail ("Missing attribute: " ^ quote name));
   1.142 -
   1.143 -fun attr x y = [(x, y)] : XML.attributes;
   1.144 -
   1.145 -fun opt_attr _ NONE = []
   1.146 -  | opt_attr name (SOME value) = attr name value;
   1.147 -
   1.148 -val pgip_id = "dummy";
   1.149 -val pgip_serial = Synchronized.counter ();
   1.150 -
   1.151 -fun output_pgip refid refseq content =
   1.152 -  XML.Elem (("pgip",
   1.153 -    attr "tag" "Isabelle/Isar" @
   1.154 -    attr "id" pgip_id @
   1.155 -    opt_attr "destid" refid @
   1.156 -    attr "class" "pg" @
   1.157 -    opt_attr "refid" refid @
   1.158 -    attr "refseq" refseq @
   1.159 -    attr "seq" (string_of_int (pgip_serial ()))), content)
   1.160 -  |> XML.string_of
   1.161 -  |> Output.urgent_message;
   1.162 -
   1.163 -
   1.164 -fun invalid_pgip () = raise Fail "Invalid PGIP packet";
   1.165 -
   1.166 -fun haspref ({name, descr, default, pgiptype, ...}: preference) =
   1.167 -  XML.Elem (("haspref", [("name", name), ("descr", descr), ("default", default)]),
   1.168 -    [XML.Elem ((pgiptype, []), [])]);
   1.169 -
   1.170 -fun process_element refid refseq (XML.Elem (("askprefs", _), _)) =
   1.171 -      get_preferences () |> List.app (fn (category, prefs) =>
   1.172 -        output_pgip refid refseq
   1.173 -          [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)])
   1.174 -  | process_element _ _ (XML.Elem (("setpref", attrs), data)) =
   1.175 -      let
   1.176 -        val name =
   1.177 -          (case Properties.get attrs "name" of
   1.178 -            SOME name => name
   1.179 -          | NONE => invalid_pgip ());
   1.180 -        val value = XML.content_of data;
   1.181 -      in set_preference name value end
   1.182 -  | process_element _ _ _ = invalid_pgip ();
   1.183 -
   1.184 -in
   1.185 -
   1.186 -fun process_pgip str =
   1.187 -  (case XML.parse str of
   1.188 -    XML.Elem (("pgip", attrs), pgips) =>
   1.189 -      let
   1.190 -        val class = get_attr attrs "class";
   1.191 -        val dest = Properties.get attrs "destid";
   1.192 -        val refid = Properties.get attrs "id";
   1.193 -        val refseq = get_attr attrs "seq";
   1.194 -        val processit =
   1.195 -          (case dest of
   1.196 -            NONE => class = "pa"
   1.197 -          | SOME id => id = pgip_id);
   1.198 -       in if processit then List.app (process_element refid refseq) pgips else () end
   1.199 -  | _ => invalid_pgip ())
   1.200 -  handle Fail msg => raise Fail (msg ^ "\n" ^ str);
   1.201 -
   1.202 -end;
   1.203 -
   1.204 -
   1.205 -(** messages **)
   1.206 -
   1.207 -(* render markup *)
   1.208 -
   1.209 -fun special ch = chr 1 ^ ch;
   1.210 -
   1.211 -local
   1.212 -
   1.213 -fun render_trees ts = fold render_tree ts
   1.214 -and render_tree t =
   1.215 -  (case XML.unwrap_elem t of
   1.216 -    SOME (_, ts) => render_trees ts
   1.217 -  | NONE =>
   1.218 -      (case t of
   1.219 -        XML.Text s => Buffer.add s
   1.220 -      | XML.Elem ((name, props), ts) =>
   1.221 -          let
   1.222 -            val (bg, en) =
   1.223 -              if null ts then Markup.no_output
   1.224 -              else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
   1.225 -              else if name = Markup.sendbackN then (special "W", special "X")
   1.226 -              else if name = Markup.intensifyN then (special "0", special "1")
   1.227 -              else if name = Markup.tfreeN then (special "C", special "A")
   1.228 -              else if name = Markup.tvarN then (special "D", special "A")
   1.229 -              else if name = Markup.freeN then (special "E", special "A")
   1.230 -              else if name = Markup.boundN then (special "F", special "A")
   1.231 -              else if name = Markup.varN then (special "G", special "A")
   1.232 -              else if name = Markup.skolemN then (special "H", special "A")
   1.233 -              else
   1.234 -                (case Markup.get_entity_kind (name, props) of
   1.235 -                  SOME kind =>
   1.236 -                    if kind = Markup.classN then (special "B", special "A")
   1.237 -                    else Markup.no_output
   1.238 -                | NONE => Markup.no_output);
   1.239 -          in Buffer.add bg #> render_trees ts #> Buffer.add en end));
   1.240 -
   1.241 -in
   1.242 -
   1.243 -fun render text =
   1.244 -  Buffer.content (render_trees (YXML.parse_body text) Buffer.empty);
   1.245 -
   1.246 -end;
   1.247 -
   1.248 -
   1.249 -(* hooks *)
   1.250 -
   1.251 -fun message bg en prfx text =
   1.252 -  (case render text of
   1.253 -    "" => ()
   1.254 -  | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
   1.255 -
   1.256 -fun setup_messages () =
   1.257 - (Output.Private_Hooks.writeln_fn := message "" "" "";
   1.258 -  Output.Private_Hooks.status_fn := (fn _ => ());
   1.259 -  Output.Private_Hooks.report_fn := (fn _ => ());
   1.260 -  Output.Private_Hooks.urgent_message_fn := message (special "I") (special "J") "";
   1.261 -  Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
   1.262 -  Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
   1.263 -  Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
   1.264 -  Output.Private_Hooks.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
   1.265 -
   1.266 -
   1.267 -(* notification *)
   1.268 -
   1.269 -val emacs_notify = message (special "I") (special "J") "";
   1.270 -
   1.271 -fun tell_clear_goals () =
   1.272 -  emacs_notify "Proof General, please clear the goals buffer.";
   1.273 -
   1.274 -fun tell_clear_response () =
   1.275 -  emacs_notify "Proof General, please clear the response buffer.";
   1.276 -
   1.277 -fun tell_file_loaded path =
   1.278 -  emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
   1.279 -
   1.280 -fun tell_file_retracted path =
   1.281 -  emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
   1.282 -
   1.283 -
   1.284 -
   1.285 -(** theory loader **)
   1.286 -
   1.287 -(* fake old ThyLoad -- with new semantics *)
   1.288 -
   1.289 -structure ThyLoad =
   1.290 -struct
   1.291 -  val add_path = Thy_Load.set_master_path o Path.explode;
   1.292 -end;
   1.293 -
   1.294 -
   1.295 -(* actions *)
   1.296 -
   1.297 -local
   1.298 -
   1.299 -fun trace_action action name =
   1.300 -  if action = Thy_Info.Update then
   1.301 -    List.app tell_file_loaded (Thy_Info.loaded_files name)
   1.302 -  else if action = Thy_Info.Remove then
   1.303 -    List.app tell_file_retracted (Thy_Info.loaded_files name)
   1.304 -  else ();
   1.305 -
   1.306 -in
   1.307 -  fun setup_thy_loader () = Thy_Info.add_hook trace_action;
   1.308 -  fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ());
   1.309 -end;
   1.310 -
   1.311 -
   1.312 -(* get informed about files *)
   1.313 -
   1.314 -(*liberal low-level version*)
   1.315 -val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
   1.316 -
   1.317 -val inform_file_retracted = Thy_Info.kill_thy o thy_name;
   1.318 -
   1.319 -fun inform_file_processed file =
   1.320 -  let
   1.321 -    val name = thy_name file;
   1.322 -    val _ = name = "" andalso error ("Bad file name: " ^ quote file);
   1.323 -    val _ =
   1.324 -      Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
   1.325 -        handle ERROR msg =>
   1.326 -          (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
   1.327 -            tell_file_retracted (Thy_Load.thy_path (Path.basic name)))
   1.328 -    val _ = Isar.init ();
   1.329 -  in () end;
   1.330 -
   1.331 -
   1.332 -(* restart top-level loop (keeps most state information) *)
   1.333 -
   1.334 -val welcome = Output.urgent_message o Session.welcome;
   1.335 -
   1.336 -fun restart () =
   1.337 - (sync_thy_loader ();
   1.338 -  tell_clear_goals ();
   1.339 -  tell_clear_response ();
   1.340 -  Isar.init ();
   1.341 -  welcome ());
   1.342 -
   1.343 -
   1.344 -(** theorem dependencies **)
   1.345 -
   1.346 -(* thm_deps *)
   1.347 -
   1.348 -local
   1.349 -
   1.350 -fun add_proof_body (PBody {thms, ...}) =
   1.351 -  thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
   1.352 -
   1.353 -fun add_thm th =
   1.354 -  (case Thm.proof_body_of th of
   1.355 -    PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
   1.356 -      if Thm.has_name_hint th andalso Thm.get_name_hint th = name
   1.357 -      then add_proof_body (Future.join body)
   1.358 -      else I
   1.359 -  | body => add_proof_body body);
   1.360 -
   1.361 -in
   1.362 -
   1.363 -fun thm_deps ths =
   1.364 -  let
   1.365 -    (* FIXME proper derivation names!? *)
   1.366 -    val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
   1.367 -    val deps = Symtab.keys (fold add_thm ths Symtab.empty);
   1.368 -  in (names, deps) end;
   1.369 -
   1.370 -end;
   1.371 -
   1.372 -
   1.373 -(* report via hook *)
   1.374 -
   1.375 -val thm_depsN = "thm_deps";
   1.376 -
   1.377 -local
   1.378 -
   1.379 -val spaces_quote = space_implode " " o map quote;
   1.380 -
   1.381 -fun thm_deps_message (thms, deps) =
   1.382 -  emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
   1.383 -
   1.384 -in
   1.385 -
   1.386 -fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
   1.387 -  if print_mode_active thm_depsN andalso
   1.388 -    can Toplevel.theory_of state andalso Toplevel.is_theory state'
   1.389 -  then
   1.390 -    let
   1.391 -      val prev_facts = Global_Theory.facts_of (Toplevel.theory_of state);
   1.392 -      val facts = Global_Theory.facts_of (Toplevel.theory_of state');
   1.393 -      val (names, deps) = thm_deps (maps #2 (Facts.dest_static [prev_facts] facts));
   1.394 -    in
   1.395 -      if null names orelse null deps then ()
   1.396 -      else thm_deps_message (spaces_quote names, spaces_quote deps)
   1.397 -    end
   1.398 -  else ());
   1.399 -
   1.400 -end;
   1.401 -
   1.402 -
   1.403 -
   1.404 -(** Isar command syntax **)
   1.405 -
   1.406 -val _ =
   1.407 -  Outer_Syntax.improper_command
   1.408 -    (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)"
   1.409 -    (Parse.text >> (fn str => Toplevel.imperative (fn () => process_pgip str)));
   1.410 -
   1.411 -val _ =
   1.412 -  Outer_Syntax.improper_command
   1.413 -    (("ProofGeneral.pr", Keyword.diag), Position.none) "print state (internal)"
   1.414 -    (Scan.succeed (Toplevel.keep (fn state =>
   1.415 -      if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
   1.416 -      else (Toplevel.quiet := false; Toplevel.print_state true state))));
   1.417 -
   1.418 -val _ = (*undo without output -- historical*)
   1.419 -  Outer_Syntax.improper_command
   1.420 -    (("ProofGeneral.undo", Keyword.control), Position.none) "(internal)"
   1.421 -    (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1)));
   1.422 -
   1.423 -val _ =
   1.424 -  Outer_Syntax.improper_command
   1.425 -    (("ProofGeneral.restart", Keyword.control), Position.none) "(internal)"
   1.426 -    (Parse.opt_unit >> (K (Toplevel.imperative restart)));
   1.427 -
   1.428 -val _ =
   1.429 -  Outer_Syntax.improper_command
   1.430 -    (("ProofGeneral.kill_proof", Keyword.control), Position.none) "(internal)"
   1.431 -    (Scan.succeed (Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
   1.432 -
   1.433 -val _ =
   1.434 -  Outer_Syntax.improper_command
   1.435 -    (("ProofGeneral.inform_file_processed", Keyword.control), Position.none) "(internal)"
   1.436 -    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_processed file)));
   1.437 -
   1.438 -val _ =
   1.439 -  Outer_Syntax.improper_command
   1.440 -    (("ProofGeneral.inform_file_retracted", Keyword.control), Position.none) "(internal)"
   1.441 -    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_retracted file)));
   1.442 -
   1.443 -
   1.444 -
   1.445 -(** init **)
   1.446 -
   1.447 -val proof_general_emacsN = "ProofGeneralEmacs";
   1.448 -
   1.449 -val initialized = Unsynchronized.ref false;
   1.450 -
   1.451 -fun init () =
   1.452 -  (if ! initialized then ()
   1.453 -   else
   1.454 -    (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
   1.455 -     Output.add_mode proof_general_emacsN
   1.456 -      Output.default_output Output.default_escape;
   1.457 -     Markup.add_mode proof_general_emacsN YXML.output_markup;
   1.458 -     setup_messages ();
   1.459 -     setup_thy_loader ();
   1.460 -     setup_present_hook ();
   1.461 -     initialized := true);
   1.462 -   sync_thy_loader ();
   1.463 -   Unsynchronized.change print_mode (update (op =) proof_general_emacsN);
   1.464 -   Secure.PG_setup ();
   1.465 -   Isar.toplevel_loop TextIO.stdIn
   1.466 -    {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
   1.467 -
   1.468 -end;
   1.469 -
   1.470 -
   1.471 -
     2.1 --- a/src/Pure/ProofGeneral/proof_general_pure.ML	Wed May 15 20:28:43 2013 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,158 +0,0 @@
     2.4 -(*  Title:      Pure/ProofGeneral/proof_general_pure.ML
     2.5 -    Author:     David Aspinall
     2.6 -    Author:     Makarius
     2.7 -
     2.8 -Proof General preferences for Isabelle/Pure.
     2.9 -*)
    2.10 -
    2.11 -(* display *)
    2.12 -
    2.13 -val _ =
    2.14 -  ProofGeneral.preference_bool ProofGeneral.category_display
    2.15 -    Printer.show_types_default
    2.16 -    "show-types"
    2.17 -    "Include types in display of Isabelle terms";
    2.18 -
    2.19 -val _ =
    2.20 -  ProofGeneral.preference_bool ProofGeneral.category_display
    2.21 -    Printer.show_sorts_default
    2.22 -    "show-sorts"
    2.23 -    "Include sorts in display of Isabelle terms";
    2.24 -
    2.25 -val _ =
    2.26 -  ProofGeneral.preference_bool ProofGeneral.category_display
    2.27 -    Goal_Display.show_consts_default
    2.28 -    "show-consts"
    2.29 -    "Show types of consts in Isabelle goal display";
    2.30 -
    2.31 -val _ =
    2.32 -  ProofGeneral.preference_option ProofGeneral.category_display
    2.33 -    @{option names_long}
    2.34 -    "long-names"
    2.35 -    "Show fully qualified names in Isabelle terms";
    2.36 -
    2.37 -val _ =
    2.38 -  ProofGeneral.preference_bool ProofGeneral.category_display
    2.39 -    Printer.show_brackets_default
    2.40 -    "show-brackets"
    2.41 -    "Show full bracketing in Isabelle terms";
    2.42 -
    2.43 -val _ =
    2.44 -  ProofGeneral.preference_bool ProofGeneral.category_display
    2.45 -    Goal_Display.show_main_goal_default
    2.46 -    "show-main-goal"
    2.47 -    "Show main goal in proof state display";
    2.48 -
    2.49 -val _ =
    2.50 -  ProofGeneral.preference_bool ProofGeneral.category_display
    2.51 -    Syntax_Trans.eta_contract_default
    2.52 -    "eta-contract"
    2.53 -    "Print terms eta-contracted";
    2.54 -
    2.55 -
    2.56 -(* advanced display *)
    2.57 -
    2.58 -val _ =
    2.59 -  ProofGeneral.preference_option ProofGeneral.category_advanced_display
    2.60 -    @{option goals_limit}
    2.61 -    "goals-limit"
    2.62 -    "Setting for maximum number of subgoals to be printed";
    2.63 -
    2.64 -val _ =
    2.65 -  ProofGeneral.preference_raw ProofGeneral.category_advanced_display
    2.66 -    (Markup.print_int o get_print_depth)
    2.67 -    (print_depth o Markup.parse_int)
    2.68 -    ProofGeneral.pgipint
    2.69 -    "print-depth"
    2.70 -    "Setting for the ML print depth";
    2.71 -
    2.72 -val _ =
    2.73 -  ProofGeneral.preference_option ProofGeneral.category_advanced_display
    2.74 -    @{option show_question_marks}
    2.75 -    "show-question-marks"
    2.76 -    "Show leading question mark of variable name";
    2.77 -
    2.78 -
    2.79 -(* tracing *)
    2.80 -
    2.81 -val _ =
    2.82 -  ProofGeneral.preference_bool ProofGeneral.category_tracing
    2.83 -    Raw_Simplifier.simp_trace_default
    2.84 -    "trace-simplifier"
    2.85 -    "Trace simplification rules";
    2.86 -
    2.87 -val _ =
    2.88 -  ProofGeneral.preference_int ProofGeneral.category_tracing
    2.89 -    Raw_Simplifier.simp_trace_depth_limit_default
    2.90 -    "trace-simplifier-depth"
    2.91 -    "Trace simplifier depth limit";
    2.92 -
    2.93 -val _ =
    2.94 -  ProofGeneral.preference_bool ProofGeneral.category_tracing
    2.95 -    Pattern.trace_unify_fail
    2.96 -    "trace-unification"
    2.97 -    "Output error diagnostics during unification";
    2.98 -
    2.99 -val _ =
   2.100 -  ProofGeneral.preference_bool ProofGeneral.category_tracing
   2.101 -    Toplevel.timing
   2.102 -    "global-timing"
   2.103 -    "Whether to enable timing in Isabelle";
   2.104 -
   2.105 -val _ =
   2.106 -  ProofGeneral.preference_bool ProofGeneral.category_tracing
   2.107 -    Toplevel.debug
   2.108 -    "debugging"
   2.109 -    "Whether to enable debugging";
   2.110 -
   2.111 -val _ =
   2.112 -  ProofGeneral.preference_raw ProofGeneral.category_tracing
   2.113 -    (fn () => Markup.print_bool (print_mode_active ProofGeneral.thm_depsN))
   2.114 -    (fn s =>
   2.115 -      if Markup.parse_bool s
   2.116 -      then Unsynchronized.change print_mode (insert (op =) ProofGeneral.thm_depsN)
   2.117 -      else Unsynchronized.change print_mode (remove (op =) ProofGeneral.thm_depsN))
   2.118 -    ProofGeneral.pgipbool
   2.119 -    "theorem-dependencies"
   2.120 -    "Track theorem dependencies within Proof General";
   2.121 -
   2.122 -
   2.123 -(* proof *)
   2.124 -
   2.125 -val _ =
   2.126 -  Unsynchronized.setmp quick_and_dirty true (fn () =>
   2.127 -    ProofGeneral.preference_bool ProofGeneral.category_proof
   2.128 -      quick_and_dirty
   2.129 -      "quick-and-dirty"
   2.130 -      "Take a few short cuts") ();
   2.131 -
   2.132 -val _ =
   2.133 -  ProofGeneral.preference_bool ProofGeneral.category_proof
   2.134 -    Goal.skip_proofs
   2.135 -    "skip-proofs"
   2.136 -    "Skip over proofs";
   2.137 -
   2.138 -val _ =
   2.139 -  Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
   2.140 -    ProofGeneral.preference_raw ProofGeneral.category_proof
   2.141 -      (Markup.print_bool o Proofterm.proofs_enabled)
   2.142 -      (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1))
   2.143 -      ProofGeneral.pgipbool
   2.144 -      "full-proofs"
   2.145 -      "Record full proof objects internally") ();
   2.146 -
   2.147 -val _ =
   2.148 -  Unsynchronized.setmp Multithreading.max_threads 0 (fn () =>
   2.149 -    ProofGeneral.preference_int ProofGeneral.category_proof
   2.150 -      Multithreading.max_threads
   2.151 -      "max-threads"
   2.152 -      "Maximum number of threads") ();
   2.153 -
   2.154 -val _ =
   2.155 -  ProofGeneral.preference_raw ProofGeneral.category_proof
   2.156 -    (fn () => Markup.print_bool (! Goal.parallel_proofs >= 1))
   2.157 -    (fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0))
   2.158 -    ProofGeneral.pgipbool
   2.159 -    "parallel-proofs"
   2.160 -    "Check proofs in parallel";
   2.161 -
     3.1 --- a/src/Pure/Pure.thy	Wed May 15 20:28:43 2013 +0200
     3.2 +++ b/src/Pure/Pure.thy	Wed May 15 20:34:42 2013 +0200
     3.3 @@ -98,7 +98,7 @@
     3.4  ML_file "Isar/isar_syn.ML"
     3.5  ML_file "Tools/find_theorems.ML"
     3.6  ML_file "Tools/find_consts.ML"
     3.7 -ML_file "ProofGeneral/proof_general_pure.ML"
     3.8 +ML_file "Tools/proof_general_pure.ML"
     3.9  
    3.10  
    3.11  section {* Further content for the Pure theory *}
     4.1 --- a/src/Pure/ROOT	Wed May 15 20:28:43 2013 +0200
     4.2 +++ b/src/Pure/ROOT	Wed May 15 20:34:42 2013 +0200
     4.3 @@ -160,7 +160,6 @@
     4.4      "Proof/proof_rewrite_rules.ML"
     4.5      "Proof/proof_syntax.ML"
     4.6      "Proof/reconstruct.ML"
     4.7 -    "ProofGeneral/proof_general.ML"
     4.8      "ROOT.ML"
     4.9      "Syntax/ast.ML"
    4.10      "Syntax/lexicon.ML"
    4.11 @@ -196,6 +195,7 @@
    4.12      "Tools/build.ML"
    4.13      "Tools/named_thms.ML"
    4.14      "Tools/legacy_xml_syntax.ML"
    4.15 +    "Tools/proof_general.ML"
    4.16      "assumption.ML"
    4.17      "axclass.ML"
    4.18      "config.ML"
     5.1 --- a/src/Pure/ROOT.ML	Wed May 15 20:28:43 2013 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Wed May 15 20:34:42 2013 +0200
     5.3 @@ -293,13 +293,10 @@
     5.4  
     5.5  use "Tools/build.ML";
     5.6  use "Tools/named_thms.ML";
     5.7 +use "Tools/proof_general.ML";
     5.8  use "Tools/legacy_xml_syntax.ML";
     5.9  
    5.10  
    5.11 -(* configuration for Proof General *)
    5.12 -use "ProofGeneral/proof_general.ML";
    5.13 -
    5.14 -
    5.15  (* ML toplevel pretty printing *)
    5.16  
    5.17  toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/Tools/proof_general.ML	Wed May 15 20:34:42 2013 +0200
     6.3 @@ -0,0 +1,468 @@
     6.4 +(*  Title:      Pure/Tools/proof_general.ML
     6.5 +    Author:     David Aspinall
     6.6 +    Author:     Makarius
     6.7 +
     6.8 +Isabelle/Isar configuration for Proof General / Emacs.
     6.9 +See also http://proofgeneral.inf.ed.ac.uk
    6.10 +*)
    6.11 +
    6.12 +signature PROOF_GENERAL =
    6.13 +sig
    6.14 +  type category = string
    6.15 +  val category_display: category
    6.16 +  val category_advanced_display: category
    6.17 +  val category_tracing: category
    6.18 +  val category_proof: category
    6.19 +  type pgiptype = string
    6.20 +  val pgipbool: pgiptype
    6.21 +  val pgipint: pgiptype
    6.22 +  val pgipfloat: pgiptype
    6.23 +  val pgipstring: pgiptype
    6.24 +  val preference_raw: category ->
    6.25 +    (unit -> string) -> (string -> unit) -> string -> string -> string -> unit
    6.26 +  val preference_bool: category -> bool Unsynchronized.ref -> string -> string -> unit
    6.27 +  val preference_int: category -> int Unsynchronized.ref -> string -> string -> unit
    6.28 +  val preference_real: category -> real Unsynchronized.ref -> string -> string -> unit
    6.29 +  val preference_string: category -> string Unsynchronized.ref -> string -> string -> unit
    6.30 +  val preference_option: category -> string -> string -> string -> unit
    6.31 +  structure ThyLoad: sig val add_path: string -> unit end
    6.32 +  val init: unit -> unit
    6.33 +  val thm_depsN: string
    6.34 +end;
    6.35 +
    6.36 +structure ProofGeneral: PROOF_GENERAL =
    6.37 +struct
    6.38 +
    6.39 +(** preferences **)
    6.40 +
    6.41 +(* type preference *)
    6.42 +
    6.43 +type category = string;
    6.44 +val category_display = "Display";
    6.45 +val category_advanced_display = "Advanced Display";
    6.46 +val category_tracing = "Tracing";
    6.47 +val category_proof = "Proof";
    6.48 +
    6.49 +type pgiptype = string;
    6.50 +val pgipbool = "pgipbool";
    6.51 +val pgipint = "pgipint";
    6.52 +val pgipfloat = "pgipint";  (*NB: PG 3.7.x and 4.0 lack pgipfloat, but accept floats as pgipint*)
    6.53 +val pgipstring = "pgipstring";
    6.54 +
    6.55 +type preference =
    6.56 + {name: string,
    6.57 +  descr: string,
    6.58 +  default: string,
    6.59 +  pgiptype: pgiptype,
    6.60 +  get: unit -> string,
    6.61 +  set: string -> unit};
    6.62 +
    6.63 +
    6.64 +(* global preferences *)
    6.65 +
    6.66 +local
    6.67 +  val preferences =
    6.68 +    Synchronized.var "ProofGeneral.preferences"
    6.69 +      ([(category_display, []),
    6.70 +        (category_advanced_display, []),
    6.71 +        (category_tracing, []),
    6.72 +        (category_proof, [])]: (category * preference list) list);
    6.73 +in
    6.74 +
    6.75 +fun add_preference category (pref: preference) =
    6.76 +  Synchronized.change preferences (map (fn (cat, prefs) =>
    6.77 +    if cat <> category then (cat, prefs)
    6.78 +    else
    6.79 +      if exists (fn {name, ...} => name = #name pref) prefs
    6.80 +      then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs))
    6.81 +      else (cat, prefs @ [pref])));
    6.82 +
    6.83 +fun get_preferences () = Synchronized.value preferences;
    6.84 +
    6.85 +end;
    6.86 +
    6.87 +fun set_preference name value =
    6.88 +  let val prefs = map (`(#name)) (maps snd (get_preferences ())) in
    6.89 +    (case AList.lookup (op =) prefs name of
    6.90 +      SOME {set, ...} => set value
    6.91 +    | NONE => error ("Unknown prover preference: " ^ quote name))
    6.92 +  end;
    6.93 +
    6.94 +
    6.95 +(* raw preferences *)
    6.96 +
    6.97 +fun preference_raw category raw_get raw_set typ name descr =
    6.98 +  let
    6.99 +    fun get () = CRITICAL raw_get;
   6.100 +    fun set x = CRITICAL (fn () => raw_set x);
   6.101 +    val pref = {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()};
   6.102 +  in add_preference category pref end;
   6.103 +
   6.104 +fun preference_ref category read write typ r =
   6.105 +  preference_raw category (fn () => read (! r)) (fn x => r := write x) typ;
   6.106 +
   6.107 +fun preference_bool category = preference_ref category Markup.print_bool Markup.parse_bool pgipbool;
   6.108 +fun preference_int category = preference_ref category Markup.print_int Markup.parse_int pgipint;
   6.109 +fun preference_real category = preference_ref category Markup.print_real Markup.parse_real pgipfloat;
   6.110 +fun preference_string category = preference_ref category I I pgipstring;
   6.111 +
   6.112 +
   6.113 +(* system options *)
   6.114 +
   6.115 +fun preference_option category option_name pgip_name descr =
   6.116 +  let
   6.117 +    val typ = Options.default_typ option_name;
   6.118 +    val pgiptype =
   6.119 +      if typ = Options.boolT then pgipbool
   6.120 +      else if typ = Options.intT then pgipint
   6.121 +      else if typ = Options.realT then pgipfloat
   6.122 +      else pgipstring;
   6.123 +  in
   6.124 +    add_preference category
   6.125 +     {name = pgip_name,
   6.126 +      descr = descr,
   6.127 +      default = Options.get_default option_name,
   6.128 +      pgiptype = pgiptype,
   6.129 +      get = fn () => Options.get_default option_name,
   6.130 +      set = Options.put_default option_name}
   6.131 +  end;
   6.132 +
   6.133 +
   6.134 +(* minimal PGIP support for <askprefs>, <haspref>, <setpref> *)
   6.135 +
   6.136 +local
   6.137 +
   6.138 +fun get_attr attrs name =
   6.139 +  (case Properties.get attrs name of
   6.140 +    SOME value => value
   6.141 +  | NONE => raise Fail ("Missing attribute: " ^ quote name));
   6.142 +
   6.143 +fun attr x y = [(x, y)] : XML.attributes;
   6.144 +
   6.145 +fun opt_attr _ NONE = []
   6.146 +  | opt_attr name (SOME value) = attr name value;
   6.147 +
   6.148 +val pgip_id = "dummy";
   6.149 +val pgip_serial = Synchronized.counter ();
   6.150 +
   6.151 +fun output_pgip refid refseq content =
   6.152 +  XML.Elem (("pgip",
   6.153 +    attr "tag" "Isabelle/Isar" @
   6.154 +    attr "id" pgip_id @
   6.155 +    opt_attr "destid" refid @
   6.156 +    attr "class" "pg" @
   6.157 +    opt_attr "refid" refid @
   6.158 +    attr "refseq" refseq @
   6.159 +    attr "seq" (string_of_int (pgip_serial ()))), content)
   6.160 +  |> XML.string_of
   6.161 +  |> Output.urgent_message;
   6.162 +
   6.163 +
   6.164 +fun invalid_pgip () = raise Fail "Invalid PGIP packet";
   6.165 +
   6.166 +fun haspref ({name, descr, default, pgiptype, ...}: preference) =
   6.167 +  XML.Elem (("haspref", [("name", name), ("descr", descr), ("default", default)]),
   6.168 +    [XML.Elem ((pgiptype, []), [])]);
   6.169 +
   6.170 +fun process_element refid refseq (XML.Elem (("askprefs", _), _)) =
   6.171 +      get_preferences () |> List.app (fn (category, prefs) =>
   6.172 +        output_pgip refid refseq
   6.173 +          [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)])
   6.174 +  | process_element _ _ (XML.Elem (("setpref", attrs), data)) =
   6.175 +      let
   6.176 +        val name =
   6.177 +          (case Properties.get attrs "name" of
   6.178 +            SOME name => name
   6.179 +          | NONE => invalid_pgip ());
   6.180 +        val value = XML.content_of data;
   6.181 +      in set_preference name value end
   6.182 +  | process_element _ _ _ = invalid_pgip ();
   6.183 +
   6.184 +in
   6.185 +
   6.186 +fun process_pgip str =
   6.187 +  (case XML.parse str of
   6.188 +    XML.Elem (("pgip", attrs), pgips) =>
   6.189 +      let
   6.190 +        val class = get_attr attrs "class";
   6.191 +        val dest = Properties.get attrs "destid";
   6.192 +        val refid = Properties.get attrs "id";
   6.193 +        val refseq = get_attr attrs "seq";
   6.194 +        val processit =
   6.195 +          (case dest of
   6.196 +            NONE => class = "pa"
   6.197 +          | SOME id => id = pgip_id);
   6.198 +       in if processit then List.app (process_element refid refseq) pgips else () end
   6.199 +  | _ => invalid_pgip ())
   6.200 +  handle Fail msg => raise Fail (msg ^ "\n" ^ str);
   6.201 +
   6.202 +end;
   6.203 +
   6.204 +
   6.205 +(** messages **)
   6.206 +
   6.207 +(* render markup *)
   6.208 +
   6.209 +fun special ch = chr 1 ^ ch;
   6.210 +
   6.211 +local
   6.212 +
   6.213 +fun render_trees ts = fold render_tree ts
   6.214 +and render_tree t =
   6.215 +  (case XML.unwrap_elem t of
   6.216 +    SOME (_, ts) => render_trees ts
   6.217 +  | NONE =>
   6.218 +      (case t of
   6.219 +        XML.Text s => Buffer.add s
   6.220 +      | XML.Elem ((name, props), ts) =>
   6.221 +          let
   6.222 +            val (bg, en) =
   6.223 +              if null ts then Markup.no_output
   6.224 +              else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
   6.225 +              else if name = Markup.sendbackN then (special "W", special "X")
   6.226 +              else if name = Markup.intensifyN then (special "0", special "1")
   6.227 +              else if name = Markup.tfreeN then (special "C", special "A")
   6.228 +              else if name = Markup.tvarN then (special "D", special "A")
   6.229 +              else if name = Markup.freeN then (special "E", special "A")
   6.230 +              else if name = Markup.boundN then (special "F", special "A")
   6.231 +              else if name = Markup.varN then (special "G", special "A")
   6.232 +              else if name = Markup.skolemN then (special "H", special "A")
   6.233 +              else
   6.234 +                (case Markup.get_entity_kind (name, props) of
   6.235 +                  SOME kind =>
   6.236 +                    if kind = Markup.classN then (special "B", special "A")
   6.237 +                    else Markup.no_output
   6.238 +                | NONE => Markup.no_output);
   6.239 +          in Buffer.add bg #> render_trees ts #> Buffer.add en end));
   6.240 +
   6.241 +in
   6.242 +
   6.243 +fun render text =
   6.244 +  Buffer.content (render_trees (YXML.parse_body text) Buffer.empty);
   6.245 +
   6.246 +end;
   6.247 +
   6.248 +
   6.249 +(* hooks *)
   6.250 +
   6.251 +fun message bg en prfx text =
   6.252 +  (case render text of
   6.253 +    "" => ()
   6.254 +  | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
   6.255 +
   6.256 +fun setup_messages () =
   6.257 + (Output.Private_Hooks.writeln_fn := message "" "" "";
   6.258 +  Output.Private_Hooks.status_fn := (fn _ => ());
   6.259 +  Output.Private_Hooks.report_fn := (fn _ => ());
   6.260 +  Output.Private_Hooks.urgent_message_fn := message (special "I") (special "J") "";
   6.261 +  Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
   6.262 +  Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
   6.263 +  Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
   6.264 +  Output.Private_Hooks.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
   6.265 +
   6.266 +
   6.267 +(* notification *)
   6.268 +
   6.269 +val emacs_notify = message (special "I") (special "J") "";
   6.270 +
   6.271 +fun tell_clear_goals () =
   6.272 +  emacs_notify "Proof General, please clear the goals buffer.";
   6.273 +
   6.274 +fun tell_clear_response () =
   6.275 +  emacs_notify "Proof General, please clear the response buffer.";
   6.276 +
   6.277 +fun tell_file_loaded path =
   6.278 +  emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
   6.279 +
   6.280 +fun tell_file_retracted path =
   6.281 +  emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
   6.282 +
   6.283 +
   6.284 +
   6.285 +(** theory loader **)
   6.286 +
   6.287 +(* fake old ThyLoad -- with new semantics *)
   6.288 +
   6.289 +structure ThyLoad =
   6.290 +struct
   6.291 +  val add_path = Thy_Load.set_master_path o Path.explode;
   6.292 +end;
   6.293 +
   6.294 +
   6.295 +(* actions *)
   6.296 +
   6.297 +local
   6.298 +
   6.299 +fun trace_action action name =
   6.300 +  if action = Thy_Info.Update then
   6.301 +    List.app tell_file_loaded (Thy_Info.loaded_files name)
   6.302 +  else if action = Thy_Info.Remove then
   6.303 +    List.app tell_file_retracted (Thy_Info.loaded_files name)
   6.304 +  else ();
   6.305 +
   6.306 +in
   6.307 +  fun setup_thy_loader () = Thy_Info.add_hook trace_action;
   6.308 +  fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ());
   6.309 +end;
   6.310 +
   6.311 +
   6.312 +(* get informed about files *)
   6.313 +
   6.314 +(*liberal low-level version*)
   6.315 +val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
   6.316 +
   6.317 +val inform_file_retracted = Thy_Info.kill_thy o thy_name;
   6.318 +
   6.319 +fun inform_file_processed file =
   6.320 +  let
   6.321 +    val name = thy_name file;
   6.322 +    val _ = name = "" andalso error ("Bad file name: " ^ quote file);
   6.323 +    val _ =
   6.324 +      Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
   6.325 +        handle ERROR msg =>
   6.326 +          (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
   6.327 +            tell_file_retracted (Thy_Load.thy_path (Path.basic name)))
   6.328 +    val _ = Isar.init ();
   6.329 +  in () end;
   6.330 +
   6.331 +
   6.332 +(* restart top-level loop (keeps most state information) *)
   6.333 +
   6.334 +val welcome = Output.urgent_message o Session.welcome;
   6.335 +
   6.336 +fun restart () =
   6.337 + (sync_thy_loader ();
   6.338 +  tell_clear_goals ();
   6.339 +  tell_clear_response ();
   6.340 +  Isar.init ();
   6.341 +  welcome ());
   6.342 +
   6.343 +
   6.344 +(** theorem dependencies **)
   6.345 +
   6.346 +(* thm_deps *)
   6.347 +
   6.348 +local
   6.349 +
   6.350 +fun add_proof_body (PBody {thms, ...}) =
   6.351 +  thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
   6.352 +
   6.353 +fun add_thm th =
   6.354 +  (case Thm.proof_body_of th of
   6.355 +    PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
   6.356 +      if Thm.has_name_hint th andalso Thm.get_name_hint th = name
   6.357 +      then add_proof_body (Future.join body)
   6.358 +      else I
   6.359 +  | body => add_proof_body body);
   6.360 +
   6.361 +in
   6.362 +
   6.363 +fun thm_deps ths =
   6.364 +  let
   6.365 +    (* FIXME proper derivation names!? *)
   6.366 +    val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
   6.367 +    val deps = Symtab.keys (fold add_thm ths Symtab.empty);
   6.368 +  in (names, deps) end;
   6.369 +
   6.370 +end;
   6.371 +
   6.372 +
   6.373 +(* report via hook *)
   6.374 +
   6.375 +val thm_depsN = "thm_deps";
   6.376 +
   6.377 +local
   6.378 +
   6.379 +val spaces_quote = space_implode " " o map quote;
   6.380 +
   6.381 +fun thm_deps_message (thms, deps) =
   6.382 +  emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
   6.383 +
   6.384 +in
   6.385 +
   6.386 +fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
   6.387 +  if print_mode_active thm_depsN andalso
   6.388 +    can Toplevel.theory_of state andalso Toplevel.is_theory state'
   6.389 +  then
   6.390 +    let
   6.391 +      val prev_facts = Global_Theory.facts_of (Toplevel.theory_of state);
   6.392 +      val facts = Global_Theory.facts_of (Toplevel.theory_of state');
   6.393 +      val (names, deps) = thm_deps (maps #2 (Facts.dest_static [prev_facts] facts));
   6.394 +    in
   6.395 +      if null names orelse null deps then ()
   6.396 +      else thm_deps_message (spaces_quote names, spaces_quote deps)
   6.397 +    end
   6.398 +  else ());
   6.399 +
   6.400 +end;
   6.401 +
   6.402 +
   6.403 +
   6.404 +(** Isar command syntax **)
   6.405 +
   6.406 +val _ =
   6.407 +  Outer_Syntax.improper_command
   6.408 +    (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)"
   6.409 +    (Parse.text >> (fn str => Toplevel.imperative (fn () => process_pgip str)));
   6.410 +
   6.411 +val _ =
   6.412 +  Outer_Syntax.improper_command
   6.413 +    (("ProofGeneral.pr", Keyword.diag), Position.none) "print state (internal)"
   6.414 +    (Scan.succeed (Toplevel.keep (fn state =>
   6.415 +      if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
   6.416 +      else (Toplevel.quiet := false; Toplevel.print_state true state))));
   6.417 +
   6.418 +val _ = (*undo without output -- historical*)
   6.419 +  Outer_Syntax.improper_command
   6.420 +    (("ProofGeneral.undo", Keyword.control), Position.none) "(internal)"
   6.421 +    (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1)));
   6.422 +
   6.423 +val _ =
   6.424 +  Outer_Syntax.improper_command
   6.425 +    (("ProofGeneral.restart", Keyword.control), Position.none) "(internal)"
   6.426 +    (Parse.opt_unit >> (K (Toplevel.imperative restart)));
   6.427 +
   6.428 +val _ =
   6.429 +  Outer_Syntax.improper_command
   6.430 +    (("ProofGeneral.kill_proof", Keyword.control), Position.none) "(internal)"
   6.431 +    (Scan.succeed (Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
   6.432 +
   6.433 +val _ =
   6.434 +  Outer_Syntax.improper_command
   6.435 +    (("ProofGeneral.inform_file_processed", Keyword.control), Position.none) "(internal)"
   6.436 +    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_processed file)));
   6.437 +
   6.438 +val _ =
   6.439 +  Outer_Syntax.improper_command
   6.440 +    (("ProofGeneral.inform_file_retracted", Keyword.control), Position.none) "(internal)"
   6.441 +    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_retracted file)));
   6.442 +
   6.443 +
   6.444 +
   6.445 +(** init **)
   6.446 +
   6.447 +val proof_general_emacsN = "ProofGeneralEmacs";
   6.448 +
   6.449 +val initialized = Unsynchronized.ref false;
   6.450 +
   6.451 +fun init () =
   6.452 +  (if ! initialized then ()
   6.453 +   else
   6.454 +    (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
   6.455 +     Output.add_mode proof_general_emacsN
   6.456 +      Output.default_output Output.default_escape;
   6.457 +     Markup.add_mode proof_general_emacsN YXML.output_markup;
   6.458 +     setup_messages ();
   6.459 +     setup_thy_loader ();
   6.460 +     setup_present_hook ();
   6.461 +     initialized := true);
   6.462 +   sync_thy_loader ();
   6.463 +   Unsynchronized.change print_mode (update (op =) proof_general_emacsN);
   6.464 +   Secure.PG_setup ();
   6.465 +   Isar.toplevel_loop TextIO.stdIn
   6.466 +    {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
   6.467 +
   6.468 +end;
   6.469 +
   6.470 +
   6.471 +
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/Tools/proof_general_pure.ML	Wed May 15 20:34:42 2013 +0200
     7.3 @@ -0,0 +1,158 @@
     7.4 +(*  Title:      Pure/Tools/proof_general_pure.ML
     7.5 +    Author:     David Aspinall
     7.6 +    Author:     Makarius
     7.7 +
     7.8 +Proof General preferences for Isabelle/Pure.
     7.9 +*)
    7.10 +
    7.11 +(* display *)
    7.12 +
    7.13 +val _ =
    7.14 +  ProofGeneral.preference_bool ProofGeneral.category_display
    7.15 +    Printer.show_types_default
    7.16 +    "show-types"
    7.17 +    "Include types in display of Isabelle terms";
    7.18 +
    7.19 +val _ =
    7.20 +  ProofGeneral.preference_bool ProofGeneral.category_display
    7.21 +    Printer.show_sorts_default
    7.22 +    "show-sorts"
    7.23 +    "Include sorts in display of Isabelle terms";
    7.24 +
    7.25 +val _ =
    7.26 +  ProofGeneral.preference_bool ProofGeneral.category_display
    7.27 +    Goal_Display.show_consts_default
    7.28 +    "show-consts"
    7.29 +    "Show types of consts in Isabelle goal display";
    7.30 +
    7.31 +val _ =
    7.32 +  ProofGeneral.preference_option ProofGeneral.category_display
    7.33 +    @{option names_long}
    7.34 +    "long-names"
    7.35 +    "Show fully qualified names in Isabelle terms";
    7.36 +
    7.37 +val _ =
    7.38 +  ProofGeneral.preference_bool ProofGeneral.category_display
    7.39 +    Printer.show_brackets_default
    7.40 +    "show-brackets"
    7.41 +    "Show full bracketing in Isabelle terms";
    7.42 +
    7.43 +val _ =
    7.44 +  ProofGeneral.preference_bool ProofGeneral.category_display
    7.45 +    Goal_Display.show_main_goal_default
    7.46 +    "show-main-goal"
    7.47 +    "Show main goal in proof state display";
    7.48 +
    7.49 +val _ =
    7.50 +  ProofGeneral.preference_bool ProofGeneral.category_display
    7.51 +    Syntax_Trans.eta_contract_default
    7.52 +    "eta-contract"
    7.53 +    "Print terms eta-contracted";
    7.54 +
    7.55 +
    7.56 +(* advanced display *)
    7.57 +
    7.58 +val _ =
    7.59 +  ProofGeneral.preference_option ProofGeneral.category_advanced_display
    7.60 +    @{option goals_limit}
    7.61 +    "goals-limit"
    7.62 +    "Setting for maximum number of subgoals to be printed";
    7.63 +
    7.64 +val _ =
    7.65 +  ProofGeneral.preference_raw ProofGeneral.category_advanced_display
    7.66 +    (Markup.print_int o get_print_depth)
    7.67 +    (print_depth o Markup.parse_int)
    7.68 +    ProofGeneral.pgipint
    7.69 +    "print-depth"
    7.70 +    "Setting for the ML print depth";
    7.71 +
    7.72 +val _ =
    7.73 +  ProofGeneral.preference_option ProofGeneral.category_advanced_display
    7.74 +    @{option show_question_marks}
    7.75 +    "show-question-marks"
    7.76 +    "Show leading question mark of variable name";
    7.77 +
    7.78 +
    7.79 +(* tracing *)
    7.80 +
    7.81 +val _ =
    7.82 +  ProofGeneral.preference_bool ProofGeneral.category_tracing
    7.83 +    Raw_Simplifier.simp_trace_default
    7.84 +    "trace-simplifier"
    7.85 +    "Trace simplification rules";
    7.86 +
    7.87 +val _ =
    7.88 +  ProofGeneral.preference_int ProofGeneral.category_tracing
    7.89 +    Raw_Simplifier.simp_trace_depth_limit_default
    7.90 +    "trace-simplifier-depth"
    7.91 +    "Trace simplifier depth limit";
    7.92 +
    7.93 +val _ =
    7.94 +  ProofGeneral.preference_bool ProofGeneral.category_tracing
    7.95 +    Pattern.trace_unify_fail
    7.96 +    "trace-unification"
    7.97 +    "Output error diagnostics during unification";
    7.98 +
    7.99 +val _ =
   7.100 +  ProofGeneral.preference_bool ProofGeneral.category_tracing
   7.101 +    Toplevel.timing
   7.102 +    "global-timing"
   7.103 +    "Whether to enable timing in Isabelle";
   7.104 +
   7.105 +val _ =
   7.106 +  ProofGeneral.preference_bool ProofGeneral.category_tracing
   7.107 +    Toplevel.debug
   7.108 +    "debugging"
   7.109 +    "Whether to enable debugging";
   7.110 +
   7.111 +val _ =
   7.112 +  ProofGeneral.preference_raw ProofGeneral.category_tracing
   7.113 +    (fn () => Markup.print_bool (print_mode_active ProofGeneral.thm_depsN))
   7.114 +    (fn s =>
   7.115 +      if Markup.parse_bool s
   7.116 +      then Unsynchronized.change print_mode (insert (op =) ProofGeneral.thm_depsN)
   7.117 +      else Unsynchronized.change print_mode (remove (op =) ProofGeneral.thm_depsN))
   7.118 +    ProofGeneral.pgipbool
   7.119 +    "theorem-dependencies"
   7.120 +    "Track theorem dependencies within Proof General";
   7.121 +
   7.122 +
   7.123 +(* proof *)
   7.124 +
   7.125 +val _ =
   7.126 +  Unsynchronized.setmp quick_and_dirty true (fn () =>
   7.127 +    ProofGeneral.preference_bool ProofGeneral.category_proof
   7.128 +      quick_and_dirty
   7.129 +      "quick-and-dirty"
   7.130 +      "Take a few short cuts") ();
   7.131 +
   7.132 +val _ =
   7.133 +  ProofGeneral.preference_bool ProofGeneral.category_proof
   7.134 +    Goal.skip_proofs
   7.135 +    "skip-proofs"
   7.136 +    "Skip over proofs";
   7.137 +
   7.138 +val _ =
   7.139 +  Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
   7.140 +    ProofGeneral.preference_raw ProofGeneral.category_proof
   7.141 +      (Markup.print_bool o Proofterm.proofs_enabled)
   7.142 +      (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1))
   7.143 +      ProofGeneral.pgipbool
   7.144 +      "full-proofs"
   7.145 +      "Record full proof objects internally") ();
   7.146 +
   7.147 +val _ =
   7.148 +  Unsynchronized.setmp Multithreading.max_threads 0 (fn () =>
   7.149 +    ProofGeneral.preference_int ProofGeneral.category_proof
   7.150 +      Multithreading.max_threads
   7.151 +      "max-threads"
   7.152 +      "Maximum number of threads") ();
   7.153 +
   7.154 +val _ =
   7.155 +  ProofGeneral.preference_raw ProofGeneral.category_proof
   7.156 +    (fn () => Markup.print_bool (! Goal.parallel_proofs >= 1))
   7.157 +    (fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0))
   7.158 +    ProofGeneral.pgipbool
   7.159 +    "parallel-proofs"
   7.160 +    "Check proofs in parallel";
   7.161 +