src/Pure/System/isar.ML
2013-05-12 ago load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;
2013-04-09 ago just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
2013-01-16 ago tuned signature;
2012-08-06 ago pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
2012-08-02 ago more official command specifications, including source position;
2012-03-16 ago outer syntax command definitions based on formal command_spec derived from theory header declarations;
2011-08-18 ago more careful treatment of exception serial numbers, with propagation to message channel;
2011-07-06 ago prefer Synchronized.var;
2010-09-09 ago main command loops are supposed to be uninterruptible -- no special treatment here;
2010-08-30 ago Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
2010-08-27 ago structure Unsynchronized is never opened and set/reset/toggle have been discontinued;
2010-08-11 ago tuned;
2010-08-09 ago Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
2010-08-03 ago find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);
2010-06-03 ago discontinued obsolete Isar.context() -- long superseded by @{context};
2010-06-01 ago uniform ML environment setup for Isar and PG;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-15 ago renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 ago refer directly to structure Keyword and Parse;
2009-10-28 ago Isar.goal: Proof.simple_goal, not raw version;
2009-10-27 ago non-critical atomic accesses;
2009-09-30 ago eliminated dead code;
2009-09-29 ago open_unsynchronized for interactive Isar loop;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-09-01 ago removed old Isar document model;
2009-06-06 ago ML_Compiler.exn_message;
2009-06-04 ago uniform (short) ids on both sides;
2009-02-28 ago fixed headers;
2009-02-28 ago moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);