src/Pure/ProofGeneral/proof_general_emacs.ML
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-03-23 wenzelm 2009-03-23 suppress status output for traditional tty modes (including Proof General); keyword report: explicitly issue message on writeln channel as well;
2009-03-05 wenzelm 2009-03-05 render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;
2009-01-05 wenzelm 2009-01-05 Isar.init;
2009-01-02 wenzelm 2009-01-02 xsymbols: use plain Symbol.output; explicit rendering of message body: print mode is always YXML, markup is only observed for singleton text (avoids overlap of inner tokens with certain status messages), test XML markup is outermost (allows Proof General font-lock); Markup.no_output;
2009-01-02 wenzelm 2009-01-02 removed print mode "PGASCII" -- 7-bit ASCII communication now always enabled;
2008-09-30 wenzelm 2008-09-30 Toplevel.commit_exit: position;
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-09-03 wenzelm 2008-09-03 theorem dependency hook: check previous state;
2008-09-03 wenzelm 2008-09-03 simplified Toplevel.add_hook: cover successful transactions only;
2008-09-02 wenzelm 2008-09-02 refined theorem dependency output: previous state needs to contain a theory (not empty toplevel); new_thms_deps: explicity theory values;
2008-09-02 wenzelm 2008-09-02 theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
2008-08-27 wenzelm 2008-08-27 get rid of tabs;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-13 wenzelm 2008-08-13 ProofDisplay.add_hook;
2008-08-11 wenzelm 2008-08-11 renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
2008-07-15 wenzelm 2008-07-15 refined Output.status_fn: priority (only visible for non-empty output, e.g. via test_markup print mode);
2008-07-15 wenzelm 2008-07-15 added status channel;
2008-07-15 wenzelm 2008-07-15 simplified commit_exit;
2008-07-14 wenzelm 2008-07-14 print_mode "test_markup": do not change prompt, otherwise Proof General will not work;
2008-07-14 wenzelm 2008-07-14 tuned message;
2008-07-14 wenzelm 2008-07-14 inform_file_processed: Isar.init_point last!
2008-07-14 wenzelm 2008-07-14 inform_file_processed: try harder not to fail, ensure
2008-07-14 wenzelm 2008-07-14 proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML); removed obsolete Toplevel.RESTART;
2008-07-10 wenzelm 2008-07-10 restart: Isar.init_point;
2008-07-10 wenzelm 2008-07-10 proper_inform_file_processed: Isar.init_point starts fresh command sequence;
2008-07-10 wenzelm 2008-07-10 activated new versions of undo, kill_proof;
2008-07-10 wenzelm 2008-07-10 added ProofGeneral.isar_kill_proof;
2008-04-17 wenzelm 2008-04-17 replaced token translations by common markup;
2008-04-14 wenzelm 2008-04-14 Isar.toplevel_loop: separate init/welcome flag;
2008-04-10 wenzelm 2008-04-10 ThyInfo.get_names;
2008-04-10 wenzelm 2008-04-10 replaced Isar loop variants by generic toplevel_loop;
2008-04-03 wenzelm 2008-04-03 moved test_markup here;
2008-04-03 wenzelm 2008-04-03 XML.output_markup;
2008-04-03 wenzelm 2008-04-03 Symbol.SOH;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-05 wenzelm 2008-03-05 IsabelleProcess.output_markup;
2008-01-06 wenzelm 2008-01-06 replaced prompt markup by prompt channel setup;
2007-12-30 wenzelm 2007-12-30 tuned;
2007-12-14 wenzelm 2007-12-14 tuned;
2007-12-06 wenzelm 2007-12-06 moved basic test_markup to isabelle_process.ML;
2007-11-19 wenzelm 2007-11-19 inform_file_processed: made even more robust against bad file specs;
2007-11-18 wenzelm 2007-11-18 removed unused inform_file_processed; proper_inform_file_processed: check before change (avoids non-linear update); avoid Path.explode here (liberal low-level file names);
2007-11-15 wenzelm 2007-11-15 thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin);
2007-10-25 wenzelm 2007-10-25 made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);
2007-10-06 wenzelm 2007-10-06 removed obsolete write_keywords;
2007-10-06 wenzelm 2007-10-06 export init_outer_syntax;
2007-10-06 wenzelm 2007-10-06 tuned;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-07 wenzelm 2007-09-07 added hilite markup;
2007-08-19 aspinall 2007-08-19 Use 376/377 specials for sendback markup
2007-08-15 wenzelm 2007-08-15 added sendback;
2007-08-13 wenzelm 2007-08-13 Lexicon.read_indexname/nat/variable;
2007-07-31 wenzelm 2007-07-31 ThyInfo.register_thy;
2007-07-22 wenzelm 2007-07-22 inform_file_processed: tuned msg, no state;
2007-07-10 wenzelm 2007-07-10 removed no_state markup -- produce empty state; Markup.add_mode;
2007-07-09 wenzelm 2007-07-09 simplified writeln_fn;
2007-07-07 wenzelm 2007-07-07 toplevel prompt/print_state: proper markup, removed hooks;