more standard document preparation within session context;

more standard document preparation within session context; more uniform document build;

more standard document preparation within session context;

clarified "isabelle logo";

clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;

less ambitious test -- terminate more quickly;

tuned;

actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;

test with many add-ons;

updated Theory.begin_theory;

entity markup for theory Pure, to enable hyperlinks etc.;

more accurate defining position of theory;

theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;

fixed theory dependency

more convenient switching of buffers;

report source path and let front-end resolve implicit master location (e.g. URL);

prefer jEdit file name representation (potentially via VFS); tuned;

more precise counting of line/column;

support for direct hyperlinks, without the Hyperlinks plugin;

tuned signature;

some markup for inlined files;

check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);

updated READMEs -- most Mac OS X problems are gone thanks to jdk-7u6;

clarified syntax boundary cases and errors;

simplified JVM startup, based on stronger assumptions about the Java version provided as Isabelle component;

eliminated obsolete byte_reader -- theory headers + body files are parsed in full;

more direct File.read_bytes -- avoid cumulative copying of StringBuilder;

improved errors of parser combinators;

tuned messages: end-of-input rarely means physical end-of-file from the past;

merged

remove Hoare dependency from Fold.thy

added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;

turned 'boogie_open' into thy_load command, without any declarations of 'uses';

tuned signature;

clarified type Token.file;

expand all files uniformly;

added build option -l (list files);

prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);

more basic file dependencies -- no load command here;

tuned signature (again, cf. ff9cd47be39b);

updated Thy_Load.check_thy;

simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;

tuned signature;

simplified Thy_Load.provide: do not store full path;

prefer ML_file over old uses; updated generated files;

merged

abstracted lemmas

prefer ML_file over old uses;

prefer ML_file over old uses;

'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';

add keywords of this node as well (e.g. relevant for Pure.thy);

tuned;

tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;

discontinued separate list of required files -- maintain only provided files as they occur at runtime; tuned signature;

find files via load commands within theory text; clarified Thy_Load.with_thy_text, simplified Thy_Load.check_thy;

clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;

pass syntax through check_thy;

use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader; tuned signatures;

clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;

tuned;

clarified bootstrapping of Pure;

tuned errors;

prefer File.full_path in accordance to check_file;

more standard Thy_Load.check_thy for Pure.thy, relying on its header; pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy; clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;

updated Thy_Load.check_thy;

refined Thy_Load.check_thy: find more uses in body text, based on keywords; refined Thy_Info.require_thy(s): cumulate additional keywords; slightly more value-oriented type Keywords.keywords;

more direct cumulation of (sparse) keywords; discontinued slightly odd patching of Pure keywords; tuned signature;

some support for thy_load_commands; clarified signatures;

tuned signature;

clarified initialization of Thy_Load, Thy_Info, Session;

tuned;

more robust cleaning of "% tag" and "-- cmt";

some support for inlining file content into outer syntax token language;

tuned comment;

tuned;

added keyword kind "thy_load" (with optional list of file extensions);

updated generated files;

more strict syntax, according to manual;

abstracted lemma

retain unknown options within preferences; tuned print;

more comprehensible platform family name;

tuned message;

fewer components, more roots;

actually remove makeall (cf. 292b97e17fb7);

tuned;

Backed out changeset ec82c33c75f8;

Typo fixed.

merged

merged

fixed lemmas

abstracted lemmas

updated to new init_components, hoping that mira can digest that;

some explanations on component categories;

specific cygwin components;

obsolete;

some explanations on isabelle components;