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;

added ISABELLE_ROOT_JVM; removed obsolete ISABELLE_HOME_JVM, ISABELLE_HOME_USER_JVM;

Theorem on polynomial division and lemmas.

removed parse_element -- no longer fits to liberal parse!

Minimalistic XML tree values.

Efficient text representation of XML trees.

added General/xml.scala, General/yxml.scala;

decode escaped symbols as well; tuned;

tuned Recoder;

more private fields;

jar: invoke scaladoc;

tuned comments; simplified symbol pattern presentation: no need to keep source strings, canonical ofString does the job; auxiliary class Recoder; proper implementation of Interpretation.decode/encode;

use scala.collection.jcl.HashMap, which seems to be more efficient; char_pattern: proper matching of surrogate unicode characters, those outside the Basic Multilingual Plane; class Interpretation: misc reorganization, more serious preparation of patterns and tables;

jar target: removed jvmpath -- does not work on Linux!?

add scala-library.jar if available;

jar target: jvmpath;

Isabelle system support.

reading symbol interpretation tables;

added Tools/isabelle_system.scala;

removed unused usage;

more robust handling of directory layout variants;

refined scala/java wrappers via isatool;

tuned abbrevs;

added ISABELLE_SCALA, ISABELLE_JAVA;

added ISABELLE_HOME_JVM;

proper jvmpath for cygwin;

proper RC;

refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;

refined JVM path wrappers;

added JVM components (Scala or Java);

tuned;

jars: build Pure.jar;

scan: proper recovery for escaped \\< symbols;

basic setup for Scala material; added General/symbol.scala;

Basic support for Isabelle symbols.

added some abbrevs; \<euro>: from default font;

removed redundant "symbol" property; added "font" propery; disabled alternative letters (\<A> etc.) for now;

Default interpretation of some Isabelle symbols.

report antiquotation names; tuned messages;

fixed DOCTYPE -- XHTML is case-sensitive!

report antiquotation names;

added ML_antiq, doc_antiq;

added README;

generated truetype font;

The Jerusalem font from 2004 -- unicode version.

args: explicit groups for file_name, theory_name;

read_asts: Lexicon.report_token, filter Lexicon.is_proper; report tokens;

filter Lexicon.is_proper -- Lexicon.tokenize now includes improper tokens;

token_kind: add Space, Comment; tokenize: now includes improper tokens, cf. is_proper; added report_token;

renamed T.source_of' to T.source_position_of; tuned signature;

renamed T.source_of' to T.source_position_of;

output_markup: check Markup.is_none;