Mercurialisabelle / file revisions
summary | shortlog | changelog | graph | tags | branches | file | revisions | annotate | diff | rss
src/Pure/ROOT.ML
2012-11-22 wenzelm 2012-11-22 more abstract Sendback operations, with explicit id/exec_id properties; purge result messages (again), cf. db58490a68ac, 7b61a539721e; file | diff | annotate
2012-10-16 wenzelm 2012-10-16 more friendly handling of Pure.thy bootstrap errors; file | diff | annotate
2012-09-25 wenzelm 2012-09-25 separate module Graph_Display; tuned signature; file | diff | annotate
2012-09-25 wenzelm 2012-09-25 added graph encode/decode operations; tuned signature; file | diff | annotate
2012-08-31 wenzelm 2012-08-31 more informative error message from failed goal forks (violating old-style TTY protocol!); file | diff | annotate
2012-08-28 wenzelm 2012-08-28 discontinued centralistic changelog; file | diff | annotate
2012-08-26 wenzelm 2012-08-26 theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing; file | diff | annotate
2012-08-22 wenzelm 2012-08-22 clarified bootstrapping of Pure; file | diff | annotate
2012-08-21 wenzelm 2012-08-21 more standard Thy_Load.check_thy for Pure.thy, relying on its header; pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy; clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current; file | diff | annotate
2012-08-20 wenzelm 2012-08-20 some support for inlining file content into outer syntax token language; file | diff | annotate
2012-08-11 wenzelm 2012-08-11 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup; file | diff | annotate
2012-08-08 wenzelm 2012-08-08 simplified Pure bootstrap -- separate pure_setup.ML was required for Alice/ML at some point; file | diff | annotate
2012-08-05 wenzelm 2012-08-05 prefer general Command_Line.tool wrapper (cf. Scala version); file | diff | annotate
2012-08-02 wenzelm 2012-08-02 more official command specifications, including source position; file | diff | annotate
2012-08-01 wenzelm 2012-08-01 more standard bootstrapping of Pure outer syntax; file | diff | annotate
2012-07-23 wenzelm 2012-07-23 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML); file | diff | annotate
2012-07-21 wenzelm 2012-07-21 some actual build function on ML side; further imitation of "usedir" shell script; file | diff | annotate
2012-05-24 wenzelm 2012-05-24 simplified Poly/ML setup -- 5.3.0 is now the common base-line; file | diff | annotate
2012-05-24 wenzelm 2012-05-24 discontinued support for Poly/ML 5.2.1; file | diff | annotate
2012-04-27 wenzelm 2012-04-27 made Context_Position independent from Config; file | diff | annotate
2012-04-04 wenzelm 2012-04-04 separate module for prover command execution; file | diff | annotate
2012-03-20 wenzelm 2012-03-20 basic support for bundled declarations; file | diff | annotate
2011-12-01 wenzelm 2011-12-01 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover; file | diff | annotate
2011-11-29 wenzelm 2011-11-29 clarified modules; file | diff | annotate
2011-11-29 wenzelm 2011-11-29 rearranged files; file | diff | annotate
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup; file | diff | annotate
2011-11-19 wenzelm 2011-11-19 added ML antiquotation @{attributes}; file | diff | annotate
2011-09-23 wenzelm 2011-09-23 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1); file | diff | annotate
2011-09-22 wenzelm 2011-09-22 abstract System_Channel in ML (cf. Scala version); back to TextIO for fifo, which is more stable in Poly/ML 5.4.x; explicit block buffering -- BinIO might be subject to old Poly/ML defaults; file | diff | annotate
2011-09-21 wenzelm 2011-09-21 slightly more general Socket_IO as part of Pure; file | diff | annotate
2011-09-04 wenzelm 2011-09-04 moved XML/YXML to src/Pure/PIDE; tuned comments; file | diff | annotate
2011-08-27 wenzelm 2011-08-27 explicit markup for legacy warnings; file | diff | annotate
2011-08-17 wenzelm 2011-08-17 more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn; file | diff | annotate
2011-08-13 wenzelm 2011-08-13 provide node header via Scala layer; clarified node edit Clear: retain header information; run_command: node info via document model, error handling within transaction; node names without ".thy" suffix, to coincide with traditional theory loader treatment; file | diff | annotate
2011-08-10 wenzelm 2011-08-10 old term operations are legacy; file | diff | annotate
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
isabelle