tuned;

refined notion of Text.Range;

decode Isabelle symbol positions in one spot;

tuned;

uniform Markup.empty/Markup.Empty in ML and Scala;

digesting strings according to SHA-1 -- Scala version;

pro-forma support for further platforms;

report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;

discontinued support for Poly/ML 5.0 and 5.1 versions;

updated for prospective Poly/ML 5.4;

multi-platform build script for Poly/ML;

updated keywords;

updated Named_Target.init;

made 9043eefe8d71 actually compile;

merged

merged

formally document `code abstype` and `code abstract` attributes

NEWS and CONTRIBUTORS

nicer code for rev

reworked section on simple datatype refinement

tuned whitespace

merged

typos in comment

more debug output

detect old Vampire and give a nicer error message

merged

now works for schematic terms as well, thanks to Alex for the `how-to'

added section on program refinement

tuned whitespace

tune;

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;

HOL-Proofs-Extraction: some workaround to make it work in low-memory situations (e.g. atbroy102 with as little as 1GB heap space);

XML.Cache: pipe-lined (thread-safe) version using actor; tuned Isabelle_Process.pid handling;

simplified internal message format: dropped special Symbol.STX header;

HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);

merged

merged

tuned section on predicate compiler

section "if something goes utterly wrong"

merged

merged

adaptation to new outline

merged

corrected handling of `constrains` elements

removed non-BSD compatible option from cp

Geoff's formatter now needs closed formulas

Using type real does not require a separate logic now.

merged

tuned text about "value" and added note on comments.

simplified command status: interpret stacked markup on demand;

event_bus.scala rather belongs to system plumbing;

some derived operations on Text.Range;

specific types Text.Offset and Text.Range; minor tuning;

moved Text_Edit to Text.Edit; tuned;

moved History/Snapshot to document.scala;

renamed raw_results to raw_protocol;

rename "unit" to "atom", to avoid confusion with the unit type;

document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;

use Synchronized.var and prevent global CRITICAL sections in this hot spot;

renamed create_id to new_id;