2011-07-11 wenzelm 2011-07-11 JVM method invocation service via Scala layer;
2011-07-10 wenzelm 2011-07-10 XML data representation of lambda terms;
2011-04-30 wenzelm 2011-04-30 railroad diagrams in LaTeX as document antiquotation;
2011-04-19 wenzelm 2011-04-19 split Type_Infer into early and late part, after Proof_Context; added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-06 wenzelm 2011-04-06 separate structure Term_Position; dismantled remains of structure Type_Ext;
2011-04-06 wenzelm 2011-04-06 renamed Standard_Syntax to Syntax_Phases;
2011-04-05 wenzelm 2011-04-05 separate module for standard implementation of inner syntax operations;
2011-04-05 wenzelm 2011-04-05 moved Isar/local_syntax.ML to Syntax/local_syntax.ML;
2011-03-27 krauss 2011-03-27 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj"; adapted test configuration SML_makeall
2011-03-20 wenzelm 2011-03-20 structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
2011-02-08 wenzelm 2011-02-08 discontinued support for Poly/ML 5.2, which was the last version without proper multithreading and TimeLimit implementation;
2011-02-05 wenzelm 2011-02-05 clarified bootstrapping of structure TimeLimit;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-11-27 wenzelm 2010-11-27 removed bash from ML system bootstrap, and past the Secure ML barrier;
2010-11-27 wenzelm 2010-11-27 more explicit Isabelle_System operations;
2010-11-06 wenzelm 2010-11-06 somewhat more uniform timing in ML vs. Scala;
2010-10-28 wenzelm 2010-10-28 added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release); refined Exn.is_interrupt: detect nested IO Interrupts; generalized Exn.map_result; more precise dependencies;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-08 haftmann 2010-09-08 removed ancient constdefs command
2010-09-01 wenzelm 2010-09-01 eliminated obsolete old-style goal stack package, which was considered the main Isabelle user interface at some point;
2010-08-27 wenzelm 2010-08-27 discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
2010-08-23 wenzelm 2010-08-23 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
2010-08-19 wenzelm 2010-08-19 moved Isar_Document to Pure/PIDE;
2010-08-17 wenzelm 2010-08-17 discontinued support for Poly/ML 5.0 and 5.1 versions;
2010-08-17 wenzelm 2010-08-17 added functor Linear_Set, based on former adhoc structures in document.ML; Linear_Set.delete_after (ML): actually delete table entries; Scala Linear_Set: clarified exceptions, according to ML version; simplified Document.node using Linear_Set; ML Document.edit: refer to start via NONE instead of no_id, according to Scala version;
2010-08-14 wenzelm 2010-08-14 moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
2010-08-11 haftmann 2010-08-11 more convenient split of class modules: class and class_declaration
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target
2010-08-11 wenzelm 2010-08-11 more precise and more maintainable dependencies;
2010-08-11 wenzelm 2010-08-11 merged, resolving conflict in src/Pure/IsaMakefile concerning General/xml_data.ML;
2010-08-10 haftmann 2010-08-10 split off structure Generic_Target into separate file
2010-08-10 wenzelm 2010-08-10 type XML.body as basic data representation language; tuned;
2010-08-05 wenzelm 2010-08-05 simplified/refined document model: collection of named nodes, without proper dependencies yet; moved basic type definitions for ids and edits from Isar_Document to Document; removed begin_document/end_document for now -- nodes emerge via edits; edits refer to named nodes explicitly;
2010-05-21 wenzelm 2010-05-21 refrain from forcing a hardwired SHELL value, cf. 1494ded298a6 but it becomes obsolete again in 549969a7f582 and follow-ups;
2010-05-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;
2010-05-15 wenzelm 2010-05-15 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
2010-05-15 wenzelm 2010-05-15 renamed structure ValueParse to Parse_Value; eliminated old-style structure alias V;
2010-05-15 wenzelm 2010-05-15 renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
2010-03-07 wenzelm 2010-03-07 Digesting strings according to SHA-1.
2010-03-07 wenzelm 2010-03-07 separate structure Typedecl;
2010-02-06 wenzelm 2010-02-06 removed ever experimental support for Moscow ML -- hardly works anymore;
2010-02-06 wenzelm 2010-02-06 explicit representation of single-assignment variables;
2010-02-06 wenzelm 2010-02-06 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
2010-01-06 wenzelm 2010-01-06 simplified build/bootstrap of Isabelle/Scala components -- avoid make;
2010-01-05 wenzelm 2010-01-05 Basic edits on plain text.
2010-01-05 wenzelm 2010-01-05 separate module Thy_Syntax for command span parsing;
2010-01-04 wenzelm 2010-01-04 omit useless (?) scaladoc;
2010-01-02 wenzelm 2010-01-02 Download URLs -- with progress monitor.
2010-01-01 wenzelm 2010-01-01 Future values -- Scala version.
2009-12-28 wenzelm 2009-12-28 separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
2009-12-22 wenzelm 2009-12-22 renamed class Outer_Keyword to Outer_Syntax; renamed tokenize to scan (cf. ML version);
2009-12-22 wenzelm 2009-12-22 Isabelle session manager -- most basic setup;
2009-12-22 wenzelm 2009-12-22 Generic parsers for Isabelle/Isar outer syntax -- Scala version.
2009-12-20 wenzelm 2009-12-20 more Scala sources;
2009-12-19 wenzelm 2009-12-19 added basic library -- Scala version; added extra support for exceptions -- Scala version; moved exn.ML to accompany exn.scala;
2009-12-18 wenzelm 2009-12-18 removed junk (cf. f49d45afa634);
2009-12-17 wenzelm 2009-12-17 Result.cache;
2009-12-04 wenzelm 2009-12-04 Basic HTML output.