more careful exception handling in order to prevent backtracking; miscellaneous tidying up.

Increasing the default limits in order to prevent unnecessary failures.

send: broadcast condition while locked!

proper signature constraint;

tuned Mailbox.send;

removed unused sync_interrupts;

moved thread data to future.ML (again); dequeue: include group; more interrupt operations; misc tuning;

more interrupt operations; maintain thread data (formerly in task_queue.ML); wait: added tracing; added requests mailbox; handle excessive workers fork: inherit group; added rudimentary shutdown; misc tuning;

moved task, thread_data, group, queue to task_queue.ML; tuned signature; SYNCHRONIZED notify_all! misc tuning;

Ordered queue of grouped tasks. formerly in future.ML; added thread data; added group; more robust dequeue: change into running here; misc tuning;

added Concurrent/task_queue.ML;

await: SYNCHRONIZED wait!

tuned check_cache; removed broken self_synchronized, which cannot be used in conjunction with condition variables; more precise use of SYNCHRONIZED vs. wait; tuned worker_loop;

added sync_interrupts, regular_interrupts; max_thread_value: enforce >= 1;

added sync_interrupts, regular_interrupts;

opaque signature constraint abstracts local type abbrev;

tuned;

added change_result;

Functional threads as future values.

added Concurrent/future.ML;

Default (mostly dummy) implementation of thread structures. formerly in multithreading.ML; create mutexes / condition variables without failure;

*** MESSAGE REFERS TO PREVIOUS VERSION *** removed dummy thread structures from multithreading.ML;

*** empty log message ***

explicit use of universal.ML and dummy_thread.ML;

added no_interrupts; tuned;

added no_interrupts; moved dummy thread structures to dummy_thread.ML;

tuned;

send: broadcast to all waiting threads;

added ML-Systems/thread_dummy.ML;

dropped "run" marker in monad syntax

multithreading.ML provides dummy thread structures;

different bookkeeping for code equations

renamed structure CodeTarget to Code_Target

instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel

proper header;

added receive_timeout; tuned comments;

check WRAPPER_OUTPUT node type;

init: disallow "" as out stream;

fixed deps: no Concurrent/receiver.ML yet;

Concurrent message exchange via mailbox -- with unbounded queueing.

added Concurrent/mailbox.ML;

reorganize subsections

rename INF_drop_prefix to INFM_drop_prefix

add lemma power_Suc2; generalize power_minus from class comm_ring_1 to ring_1

move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add

tuned signature;

added General/queue.ML;

Efficient queues.

moved Multithreading.task/schedule to Concurrent/schedule.ML

multithreading.ML provides dummy thread structures;

moved Multithreading.task/schedule to Concurrent/schedule.ML;

provide dummy thread structures, including proper Thread.getLocal/setLocal; moved task/schedule to Concurrent/schedule.ML;

Thread.getLocal/setLocal;

Scheduling -- multiple threads working on a queue of tasks. formerly in ML-Systems/multithreading_polyml.ML; simplified -- less tracing; use regular Isabelle/ML functions instead of NJ stuff;

added Concurrent/schedule.ML;

update tags

use /home/isabelle/mercurial/bin/hg wrapper;

exclude large .mov files;

simplified add_axiom: no hyps;

discontinued local axioms -- too difficult to implement, too easy to produce nonsense;

axiomatization is now global-only;

added const_decl;

simplified specify_const: canonical args, global deps;

declare_const: Name.binding, store/report position;

Sign.declare_const: Name.binding;

removed ex/Puzzle

added qualified: string -> binding -> binding;

Name.qualified;

theorem dependency hook: check previous state;

added pos_of;

-> AFP

simplified Toplevel.add_hook: cover successful transactions only;

retired Ben Porter's DenumRat in favour of the shorter proof in Real/Rational.thy

made SML/NJ happy;

refined theorem dependency output: previous state needs to contain a theory (not empty toplevel); new_thms_deps: explicity theory values;

* Generic Toplevel.add_hook interface allows to analyze the result of transactions (including failed ones). For example, see src/Pure/ProofGeneral/proof_general_pgip.ML for theorem dependency output of transactions resulting in a new theory state.

Replaced Library/NatPair by Nat_Int_Bij.

added new_thms_deps (operates on global facts, some name_hint approximation); theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;

theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;

added add_hook interface for post-transition hooks;

tuned;

ProofDisplay.print_results;

no pervasive bindings; removed theory_results and related hook; print_results: ignore empty/internal kind -- like former theory_results;

Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and distributed them over Real/ (to do with bijections and density). Library/NatPair became Nat_Int_Bij and made that part of Main.

distributed literal code generation out of central infrastructure

* Result facts now refer to the *full* internal name;

* Name bindings in higher specification mechanisms;

pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);

updated generated file;

Interpretation commands no longer accept interpretation attributes.

type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;

explicit type Name.binding for higher-specification elements;

explicit type Name.binding for higher-specification elements; report local_fact_decl, fixed_decl; simplified ProofContext.inferred_param;

explicit type Name.binding for higher-specification elements; added binding, parbinding;

explicit type Name.binding for higher-specification elements; simplified ProofContext.inferred_param;

explicit type Name.binding for higher-specification elements; name/var morphism operates on Name.binding;

added binding; thm_name/opt_thm_name: Name.binding;

added fixed_decl, fact_decl, local_fact_decl;

name_thm etc.: pass position; note_thms etc.: Name.binding, report fact_decl;

added type binding -- generic name bindings;

name/var morphism operates on Name.binding;

adapted to class instantiation compliance

It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...

renamed lemma

moved more lemmas here from AFP/Integration/Rats

moved lemma into SetInterval where it belongs

cleaned up code generation for {.._} and {..<_} moved lemmas into SetInterval where they belong

*** empty log message ***

extended interface to preferences to allow adding new ones

Prover is set via menu now

restructured code generation of literals

IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo; IsabelleSystem.exec: varargs convenience; more robust message thread management: no interrupt, but proper rendezvous via fifo (rm_fifo removes unused fifo, if isabelle-process fails);

init: more explicit protocol of open/remove rendezvous;

use hardwired /tmp -- fifo only work on local file-system;

separate module for code output

fixed names of class assumptions

dropped parameter prefix for class theorems

added charset (from isabelle_process.scala); added fifo_reader -- also works on Cygwin;

moved charset to isabelle_system.scala; IsabelleSystem.fifo_reader;

provide HOME_JVM=HOME to prevent implicit cygpath mangling;

restructured and split code serializer module

no parameter prefix for class interpretation

updated

tuned fold_lines;

fold_lines: simplified, more efficient due to String.fields;

rm fifo after open;

dummy setup for completion;

create named pipe;

added is_cygwin; added exec2, which joins stdout/stderr; tuned thread arrangement;

join stdout/stderr, eliminated Kind.STDERR; messages are read from separate fifo (ensures that spurious stdout from shell wrappers, Poly/ML runtime system etc. do not spoil message protocol); private output, output_raw;

explicit output stream, typically a named pipe;

refined option -W: output stream;

more function -> fun

quicksort: function -> fun

corrected some typos

fixed atom_to_xml: literal "name" attribute;

exported atom_to_xml;

changed Markup print mode to YXML -- explicitly decode messages before being issued; changed Output print mode to plain default -- no escaping; simplified pgml_sym: produce Pgml.pgmlatom, no special treatment of Ctrl/Raw; removed unused issue_pgips; removed obsolete delay_msgs feature -- the script parser never fails, but produces inline error markup; removed obsolete wrap_pgml; explicit transformation of messages (pgml_terms and message_content); remove obsolete split_markup workaround; misc tuning;

tuned;

present_token: disable print_mode, which is YXML now;

text_of Malformed: explode with spaces -- Output.output/escape ineffective by default;

removed obsolete XML.Output workaround;

added get_int;

removed obsolete get_string; moved get_int to property.ML;

removed obsolete ProofGeneral/pgml_isabelle.ML;

simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)

renamed Buffer.write to File.write_buffer; added scalable iterator fold_lines; tuned;

renamed Buffer.write to File.write_buffer;

load buffer.ML before file.ML;

replaced find_substring by first_field;

Consistent naming of theorems in interpretation.

simplified parse_attrib (find_substring instead of space_explode);

added find_substring;

added HOL/ex/Numeral.thy

get rid of tabs;

Property lists.

added General/properties.ML;

type Properties.T;

proper error message

proper handling of type variabl names

completing arities after subclass instance

untabification

tuned code generator setup

added equivariance lemmas for ex1 and the

add lemmas about Rats similar to those about Reals

move real_vector class proofs into vector_space and group_hom locales

added distributivity of relation composition over union [simp]

tuned append;

command: symbols.encode;

Reorganisation of registration code.

function package: name primitive defs "f_sumC_def" instead of "f_sum_def" to avoid clashes

purge classes after compilation;

renamed Isabelle-repository to isabelle;

Defined rationals (Rats) globally in Rational. Chractarized them with a few lemmas in RealDef, one of them from Sqrt.

replaced /home/isabelle/html-data/isabelle-repos by /home/isabelle-repository/repos;

moved new Symbol.Interpretation into plugin;

promoted to EBPlugin; tuned;

explicitly depend on isabelle-Pure.jar and isabelle-scala-library.jar;

tuned;

isabelle process: pick options/args from properties;

removed unused ConsolePlugin dependency; added menu item; added some Isabelle options;

simplified exceptions: use plain error function / RuntimeException;

added try_result;

misc reorganization; simplified consumer thread; more robust stop;

Kind: added is_control; more robust kill/exit; tuned interfaces;

get: allow null;

misc tuning of names;

rearranged source files;

init_message: class markup in message body, not header;

repackaged as isabelle.jedit;

untabify: silently turn tab into space if column information is unavailable;

corrected cache handling for class operations

default replaces arbitrary

tuned import order

activated \<A>, \<a>, \<AA>, \<aa>; disabled \<RR>, \<II> which overlap with codepoints for \<Re>, \<Im>, remapped to unofficial place within Isabelle font;

* Isabelle/lib/classes/Pure.jar; * Status messages; * Homegrown Isabelle font;

jars: removed obsolete Java process wrapper (cf. new Pure.jar);

obsolete;

obsolete -- superceded by Pure.jar (Scala version);

updated to Pure.jar;

added exec; private posix_prefix;

moved class Result into static object, removed dynamic tree method; removed unused Symbol.Interpretation; class Result: added is_raw, is_system; disabled console echo; added interrupt, kill; IsabelleSystem.exec;

symbolic message markup; init message: class property;

renamed Markup.MALFORMED to Markup.BAD;

added position, messages; renamed messages to content, malformed to bad;

added messages and process information;

Position properties.

added General/position.scala;

adapted to new IsabelleProcess from Pure.jar; IsabellePlugin.result_content decodes symbols;

include ../../classes/Pure.jar;

added const Rational added more function puzzles

YXML.parse_failsafe; removed full_markup, YXML mode (default); renamed output_command to command; renamed output_ML to ML; tuned;

shell_prefix: physical /bin/env on Cygwin;

removed full_markup mode (default); removed YXML mode (default); added XML mode; message: class attribute, fail for malformed YXML;

added parse_failsafe;

refer to symbolic Markup;

Common markup elements.

added General/markup.scala;

BadVariable: toString;

use java.util.concurrent.LinkedBlockingQueue, which blocks as required; IsabelleProcessException: toString; Result: improved toString; Result: raw markup for stdout/stderr; cmdline: proper executable name, added YXML mode;

append_string: proper backslash in character escapes;

added getenv; renamed get_setting to getenv_strict; added shell_prefix (for Cygwin);

tuned;

Isabelle outer syntax.

added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala; scalac -deprecation;

Isabelle process management -- always reactive due to multi-threaded I/O.

renamed DOM to document, add xml version and optional stylesheets;

tuned comments; added document object model (DOM);

parse_attrib: proper index of name end!

tuned parse performance: avoid splitting terminal Y chunk;

parse_attrib: more efficient due to indexOf('=');

replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);

tuned comment;

added iterator over content;

proper ISABELLE_ROOT_JVM on Cygwin;

pattern: proper "." not "[.]"! tuned;

recode: proper result for unmatched symbols;

more robust pattern: look at longer matches first, added catch-all case; more private fields; reworked Recoder: more direct char/string operations, avoids inefficiency of large alternatives (java.util.regex does not optimize regexps);

added get_setting; removed obsolete ISABELLE_HOME, ISABELLE_HOME_USER; added platform_path, which expands variables and performs basic cygwin conversion;

read_symbols: proper IsabelleSystem.platform_path;