2014-04-19 wenzelm [Sat, 19 Apr 2014 17:23:05 +0200] rev 56618
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
NEWS etc/isar-keywords-ZF.el etc/isar-keywords.el src/Pure/Isar/isar_syn.ML src/Pure/ML/ml_compiler.ML src/Pure/ML/ml_compiler_polyml.ML src/Pure/ML/ml_env.ML src/Pure/Pure.thy src/Pure/pure_syn.ML src/Tools/Code/code_runtime.ML src/Tools/SML/Examples.thy

2014-04-17 wenzelm [Thu, 17 Apr 2014 14:52:23 +0200] rev 56617
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
src/Pure/System/isabelle_process.scala

2014-04-17 wenzelm [Thu, 17 Apr 2014 13:21:36 +0200] rev 56616
added protocol command "use_theories", with core functionality of batch build;
src/Pure/PIDE/markup.ML src/Pure/PIDE/markup.scala src/Pure/PIDE/protocol.ML src/Pure/PIDE/protocol.scala

2014-04-17 wenzelm [Thu, 17 Apr 2014 12:03:15 +0200] rev 56615
tuned comments;
src/Pure/Tools/build.ML

2014-04-17 wenzelm [Thu, 17 Apr 2014 11:42:36 +0200] rev 56614
tuned;
src/Pure/Thy/present.ML src/Pure/Tools/build.ML

2014-04-17 wenzelm [Thu, 17 Apr 2014 11:31:46 +0200] rev 56613
tuned option name;
etc/options src/Pure/Tools/find_theorems.ML

2014-04-17 wenzelm [Thu, 17 Apr 2014 11:29:15 +0200] rev 56612
tuned;
src/Pure/Thy/present.ML src/Pure/Tools/build.ML

2014-04-17 wenzelm [Thu, 17 Apr 2014 11:13:30 +0200] rev 56611
proper tooltip_lines for multi-line text;
src/Tools/jEdit/src/jedit_options.scala src/Tools/jEdit/src/spell_checker.scala

2014-04-17 wenzelm [Thu, 17 Apr 2014 10:58:10 +0200] rev 56610
unused;
src/Pure/General/word.scala

2014-04-17 wenzelm [Thu, 17 Apr 2014 10:54:10 +0200] rev 56609
capitalize more carefully, e.g. relevant for option "ML_exception_trace";
src/Pure/General/word.scala src/Pure/System/options.scala src/Tools/jEdit/src/isabelle_sidekick.scala src/Tools/jEdit/src/symbols_dockable.scala