src/Pure/ROOT.ML
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-30 wenzelm 2010-08-30 more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
2010-08-23 wenzelm 2010-08-23 recognize more "smlnj" variants;
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-15 wenzelm 2010-08-15 more explicit / functional ML version of document model; tuned;
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 haftmann 2010-08-11 merged
2010-08-11 haftmann 2010-08-11 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
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-11 wenzelm 2010-08-11 Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
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-07-24 wenzelm 2010-07-24 moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state; theory loader: reduced warnings -- thy database can be bypassed in certain situations; Proof/Local_Theory.propagate_ml_env; ML use function: propagate ML environment as well; pervasive type generic_theory;
2010-07-12 wenzelm 2010-07-12 removed legacy aliases;
2010-06-01 wenzelm 2010-06-01 uniform ML environment setup for Isar and PG;
2010-06-01 wenzelm 2010-06-01 keep structure ThyLoad for the sake of Proof General;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-18 wenzelm 2010-05-18 do not open Legacy by default;
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-17 wenzelm 2010-05-17 centralized legacy aliases;
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-24 wenzelm 2010-03-24 slightly more logical bootstrap order -- also helps to sort out proof terms extension;
2010-03-09 wenzelm 2010-03-09 added ProofContext.tsig_of -- proforma version for local name space only, not logical content; added ProofContext.read_type_name_proper; localized ProofContext.read_class/read_arity/cert_arity; localized ProofContext.class_space/type_space etc.;
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 explicit representation of single-assignment variables;
2009-11-09 wenzelm 2009-11-09 setup for official Poly/ML 5.3.0, which is now the default;
2009-11-01 wenzelm 2009-11-01 Rules that characterize functional/relational specifications.
2009-10-01 wenzelm 2009-10-01 Concurrently cached values.
2009-10-01 wenzelm 2009-10-01 more official status of sequential implementations; tuned;
2009-10-01 wenzelm 2009-10-01 separate concurrent/sequential versions of lazy evaluation; lazy based on future avoids wasted evaluations;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-28 wenzelm 2009-09-28 Dummy version of state variables -- plain refs for sequential access.
2009-08-11 wenzelm 2009-08-11 clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
2009-07-25 wenzelm 2009-07-25 renamed structure Display_Goal to Goal_Display;
2009-07-24 wenzelm 2009-07-24 renamed Pure/tctical.ML to Pure/tactical.ML;
2009-07-20 wenzelm 2009-07-20 moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
2009-07-16 wenzelm 2009-07-16 Support for copy-avoiding functions on pure values, at the cost of readability.
2009-06-06 wenzelm 2009-06-06 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
2009-06-04 wenzelm 2009-06-04 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
2009-06-02 wenzelm 2009-06-02 early setup of secure operations (again, cf. deddd77112b7) -- NB: fix_ints is required for bootstrap; late setup of ML_Env and ML_Compiler;
2009-06-01 wenzelm 2009-06-01 added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
2009-06-01 wenzelm 2009-06-01 slightly later setup of ML and secure operations;
2009-04-01 wenzelm 2009-04-01 tuned comments;
2009-03-22 wenzelm 2009-03-22 ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;
2009-03-17 wenzelm 2009-03-17 turned structure NetRules into general Item_Net, which is loaded earlier;
2009-02-28 wenzelm 2009-02-28 moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-31 wenzelm 2008-12-31 added old_term.ML;
2008-12-15 haftmann 2008-12-15 moved value.ML to src/Tools
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code