2010-08-10 wenzelm 2010-08-10 type XML.body as basic data representation language; tuned;
2010-08-10 wenzelm 2010-08-10 renamed YXML.binary_text to YXML.escape_controls to emphasize what it actually does;
2010-08-10 wenzelm 2010-08-10 added string_bytes convenience;
2010-08-10 wenzelm 2010-08-10 tuned;
2010-08-10 wenzelm 2010-08-10 removed obsolete methods for (ML) commands;
2010-08-10 wenzelm 2010-08-10 prefer Nimbus look and feel on all platforms, instead of the somewhat ugly javax.swing.plaf.metal.MetalLookAndFeel, which presumably is implicit fall-back nonetheless;
2010-08-10 wenzelm 2010-08-10 edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;
2010-08-10 wenzelm 2010-08-10 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names; asynchronous Isabelle_Process.init -- raw ML toplevel stays active; simplified Isabelle_Process using actors; misc tuning;
2010-08-10 wenzelm 2010-08-10 added Library.thread_actor -- thread as actor;
2010-08-10 wenzelm 2010-08-10 clarified JEDIT_JAVA_OPTIONS vs. JEDIT_SYSTEM_OPTIONS -- discontinued JEDIT_APPLE_PROPERTIES; static default Dactors.corePoolSize=4 for more reproducible concurrency, independently of number of cores;
2010-08-09 wenzelm 2010-08-09 auto_flush: higher frequency;
2010-08-09 wenzelm 2010-08-09 uniform raw_dump for input/output fifos on Cygwin;
2010-08-09 wenzelm 2010-08-09 more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;
2010-08-09 wenzelm 2010-08-09 Isabelle_Process: separate input fifo for commands (still using the old tty protocol); some partial workarounds for Cygwin;
2010-08-09 wenzelm 2010-08-09 tuned comments;
2010-08-09 wenzelm 2010-08-09 merged
2010-08-09 haftmann 2010-08-09 added Lars Noschinski to isatest report
2010-08-09 wenzelm 2010-08-09 merged
2010-08-08 haftmann 2010-08-08 discontinued separation of `define` and `declare_const`
2010-08-08 haftmann 2010-08-08 unravelled target initialization code
2010-08-08 boehmes 2010-08-08 added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
2010-08-08 boehmes 2010-08-08 added scanning of if-then-else expressions
2010-08-06 blanchet 2010-08-06 merged
2010-08-06 blanchet 2010-08-06 added support for partial quotient types; previously Nitpick was unsound for these
2010-08-06 blanchet 2010-08-06 adapt occurrences of renamed Nitpick functions
2010-08-06 blanchet 2010-08-06 document the non-legacy interfaces
2010-08-06 blanchet 2010-08-06 local versions of Nitpick.register_xxx functions
2010-08-08 wenzelm 2010-08-08 parse_spans: somewhat faster low-level implementation;
2010-08-08 wenzelm 2010-08-08 proper context for Syntax.parse_token;
2010-08-08 wenzelm 2010-08-08 prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
2010-08-08 wenzelm 2010-08-08 explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-08-08 wenzelm 2010-08-08 fixed odd runtime type error, which appears to have escaped the scala-2.8.0.final compiler;
2010-08-08 wenzelm 2010-08-08 YXML.parse: refrain from interning, let XML.Cache do it (partially);
2010-08-08 wenzelm 2010-08-08 cache_string: store trimmed string value;
2010-08-07 wenzelm 2010-08-07 simple_dialog: allow scala.swing.Component as well;
2010-08-07 wenzelm 2010-08-07 simplified some Markup;
2010-08-07 wenzelm 2010-08-07 simplified type XML.Tree: embed Markup directly, avoid slightly odd triple; XML.cache_tree: actually store XML.Text as well; added Isabelle_Process.Result.properties;
2010-08-07 wenzelm 2010-08-07 more robust treatment of Markup.token;
2010-08-07 wenzelm 2010-08-07 simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
2010-08-07 wenzelm 2010-08-07 concentrate structural document notions in document.scala; tuned;
2010-08-07 wenzelm 2010-08-07 maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
2010-08-07 wenzelm 2010-08-07 tuned;
2010-08-07 wenzelm 2010-08-07 more explicit model of pending text edits;
2010-08-07 wenzelm 2010-08-07 more explicit treatment of Swing thread context; Document_Model.snapshot: require Swing thread;
2010-08-07 wenzelm 2010-08-07 replaced individual Document_Model history by all-inclusive one in Session; Document_Model: provide thy_name externally, i.e. by central Isabelle plugin; tuned;
2010-08-07 wenzelm 2010-08-07 misc tuning and clarification;
2010-08-06 wenzelm 2010-08-06 avoid null in Scala; tuned comments;
2010-08-06 wenzelm 2010-08-06 updated keywords;
2010-08-06 wenzelm 2010-08-06 removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
2010-08-06 wenzelm 2010-08-06 merged
2010-08-06 blanchet 2010-08-06 merged
2010-08-06 blanchet 2010-08-06 quotient types registered as codatatypes are no longer quotient types
2010-08-06 blanchet 2010-08-06 added a friendly warning
2010-08-06 blanchet 2010-08-06 extend the scope of limitation about nonconservative extensions
2010-08-06 blanchet 2010-08-06 improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
2010-08-05 ballarin 2010-08-05 Remove duplicate locale activation code; performance improvement.
2010-08-05 blanchet 2010-08-05 added record field
2010-08-05 blanchet 2010-08-05 added "whack"
2010-08-05 blanchet 2010-08-05 handle "Rep_unit" & Co. gracefully
2010-08-05 blanchet 2010-08-05 added support for "Abs_" and "Rep_" functions on quotient types