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;

more explicit / functional ML version of document model; tuned;

renamed class Document to Document.Version etc.; renamed Change.prev to Change.previous, and Change.document to Change.current; tuned;

fixed Isabelle/Scala build (cf. f3220ef79d51);

Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;

more basic Markup.parse_int/print_int (using signed_string_of_int) (ML); added convenient Markup.Int/Long objects (Scala); simplified "assign" message format -- explicit version id; misc tuning and simplification;

Keyword.status: always suppress position;

moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;

merged

robustified proof

lemma execute_bind_case

unit and bool are instances of heap

merged

sketch of new outline

sketch of new outline

ditem

refined abstract

added stub "If something utterly fails"

avoid variable name acc (cf. cs. 3142c1e21a0e)

import swap prevents strange failure of SML code generator for datatypes

added setup

merged

group record-related ML files

merged

dropped dead code

moved Record.thy from session Plain to Main; avoid variable name acc

group record-related ML files

Class.declare -> Class.const

named target is optional; explicit Name_Target.reinit

named target is optional

Named_Target.init: empty string represents theory target

Named_Target.theory_init

simplified code

tuned

tuned

merged

tuned whitespace

tuned internal structure

remove reinit operation alltogether

avoid arcane Local_Theory.reinit entirely

more convenient split of class modules: class and class_declaration

tuned

stripped signature

explicit accessed to structure Class_Target

tuned lowercase

moved Document.text_edits to Thy_Syntax;

tuned;

added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);

do not buffer fifo streams here -- done in Isabelle_Process; removed misleading comments -- blocking on open is not reliable on non-standard systems (Cygwin);

explicit Document.State value, instead of individual state variables in Session, Command, Document; Session.snapshot: pure value based on Document.State; Document.edit_texts: no treatment of state assignment here;