2011-08-10 |
wenzelm |
2011-08-10 |
moved old code generator to src/Tools/;
|
file | diff | annotate |
2011-08-08 |
wenzelm |
2011-08-08 |
modernized file proof_checker.ML;
|
file | diff | annotate |
2011-07-23 |
wenzelm |
2011-07-23 |
explicit structure ML_System;
tunned ML bootstrap;
|
file | diff | annotate |
2011-07-16 |
wenzelm |
2011-07-16 |
moved bash operations to Isabelle_System (cf. Scala version);
|
file | diff | annotate |
2011-07-16 |
wenzelm |
2011-07-16 |
more general bash_process, which allows to terminate background processes as well;
|
file | diff | annotate |
2011-07-13 |
wenzelm |
2011-07-13 |
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
|
file | diff | annotate |
2011-07-13 |
wenzelm |
2011-07-13 |
sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
minor tuning;
|
file | diff | annotate |
2011-07-13 |
wenzelm |
2011-07-13 |
XML.pretty with depth limit;
|
file | diff | annotate |
2011-07-12 |
wenzelm |
2011-07-12 |
discontinued obsolete Isabelle_Syntax and Parse_Value -- superseded by Outer_Syntax.quote_string and XML.Encode, Term_XML.Encode etc.;
|
file | diff | annotate |
2011-07-12 |
wenzelm |
2011-07-12 |
tuned XML modules;
|
file | diff | annotate |
2011-07-11 |
wenzelm |
2011-07-11 |
JVM method invocation service via Scala layer;
|
file | diff | annotate |
2011-07-11 |
wenzelm |
2011-07-11 |
some support for raw messages, which bypass standard Symbol/YXML decoding;
tuned signature;
|
file | diff | annotate |
2011-07-10 |
wenzelm |
2011-07-10 |
XML data representation of lambda terms;
|
file | diff | annotate |
2011-07-08 |
wenzelm |
2011-07-08 |
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
tuned signatures;
tuned module dependencies;
|
file | diff | annotate |
2011-07-06 |
wenzelm |
2011-07-06 |
prefer Synchronized.var;
|
file | diff | annotate |
2011-06-29 |
wenzelm |
2011-06-29 |
print Path.T with some markup;
|
file | diff | annotate |
2011-06-25 |
wenzelm |
2011-06-25 |
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
|
file | diff | annotate |
2011-04-30 |
wenzelm |
2011-04-30 |
railroad diagrams in LaTeX as document antiquotation;
|
file | diff | annotate |
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;
|
file | diff | annotate |
2011-04-18 |
wenzelm |
2011-04-18 |
simplified pretty printing context, which is only required for certain kernel operations;
disentangled dependencies of structure Pretty;
|
file | diff | annotate |
2011-04-17 |
wenzelm |
2011-04-17 |
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
|
file | diff | annotate |
2011-04-16 |
wenzelm |
2011-04-16 |
tuned signature, disentangled dependencies;
|
file | diff | annotate |
2011-04-08 |
wenzelm |
2011-04-08 |
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
clarified Syntax.root;
|
file | diff | annotate |
2011-04-08 |
wenzelm |
2011-04-08 |
explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;
|
file | diff | annotate |
2011-04-06 |
wenzelm |
2011-04-06 |
separate structure Term_Position;
dismantled remains of structure Type_Ext;
|
file | diff | annotate |
2011-04-06 |
wenzelm |
2011-04-06 |
renamed Standard_Syntax to Syntax_Phases;
|
file | diff | annotate |
2011-04-05 |
wenzelm |
2011-04-05 |
separate module for standard implementation of inner syntax operations;
|
file | diff | annotate |
2011-04-05 |
wenzelm |
2011-04-05 |
moved Isar/local_syntax.ML to Syntax/local_syntax.ML;
|
file | diff | annotate |
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;
|
file | diff | annotate |
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;
|
file | diff | annotate |
2011-02-05 |
wenzelm |
2011-02-05 |
clarified bootstrapping of structure TimeLimit;
|
file | diff | annotate |
2010-12-17 |
wenzelm |
2010-12-17 |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file | diff | annotate |
2010-11-27 |
wenzelm |
2010-11-27 |
removed bash from ML system bootstrap, and past the Secure ML barrier;
|
file | diff | annotate |
2010-11-27 |
wenzelm |
2010-11-27 |
more explicit Isabelle_System operations;
|
file | diff | annotate |
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;
|
file | diff | annotate |
2010-09-17 |
wenzelm |
2010-09-17 |
simplified some internal flags using Config.T instead of full-blown Proof_Data;
|
file | diff | annotate |
2010-09-12 |
wenzelm |
2010-09-12 |
load type_infer.ML later -- proper context for Type_Infer.infer_types;
renamed Type_Infer.polymorphicT to Type.mark_polymorphic;
|
file | diff | annotate |
2010-09-08 |
haftmann |
2010-09-08 |
removed ancient constdefs command
|
file | diff | annotate |
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;
|
file | diff | annotate |
2010-08-30 |
wenzelm |
2010-08-30 |
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
|
file | diff | annotate |
2010-08-23 |
wenzelm |
2010-08-23 |
recognize more "smlnj" variants;
|
file | diff | annotate |
2010-08-19 |
wenzelm |
2010-08-19 |
moved Isar_Document to Pure/PIDE;
|
file | diff | annotate |
2010-08-17 |
wenzelm |
2010-08-17 |
discontinued support for Poly/ML 5.0 and 5.1 versions;
|
file | diff | annotate |
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;
|
file | diff | annotate |
2010-08-15 |
wenzelm |
2010-08-15 |
more explicit / functional ML version of document model;
tuned;
|
file | diff | annotate |
2010-08-14 |
wenzelm |
2010-08-14 |
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
|
file | diff | annotate |
2010-08-11 |
haftmann |
2010-08-11 |
more convenient split of class modules: class and class_declaration
|
file | diff | annotate |
2010-08-11 |
haftmann |
2010-08-11 |
renamed Theory_Target to the more appropriate Named_Target
|
file | diff | annotate |
2010-08-11 |
haftmann |
2010-08-11 |
merged
|
file | diff | annotate |
2010-08-11 |
haftmann |
2010-08-11 |
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
|
file | diff | annotate |
2010-08-11 |
wenzelm |
2010-08-11 |
merged, resolving conflict in src/Pure/IsaMakefile concerning General/xml_data.ML;
|
file | diff | annotate |
2010-08-10 |
haftmann |
2010-08-10 |
split off structure Generic_Target into separate file
|
file | diff | annotate |
2010-08-11 |
wenzelm |
2010-08-11 |
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
|
file | diff | annotate |
2010-08-10 |
wenzelm |
2010-08-10 |
type XML.body as basic data representation language;
tuned;
|
file | diff | annotate |
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;
|
file | diff | annotate |
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;
|
file | diff | annotate |
2010-07-12 |
wenzelm |
2010-07-12 |
removed legacy aliases;
|
file | diff | annotate |
2010-06-01 |
wenzelm |
2010-06-01 |
uniform ML environment setup for Isar and PG;
|
file | diff | annotate |
2010-06-01 |
wenzelm |
2010-06-01 |
keep structure ThyLoad for the sake of Proof General;
|
file | diff | annotate |
2010-05-31 |
wenzelm |
2010-05-31 |
modernized some structure names, keeping a few legacy aliases;
|
file | diff | annotate |