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;