ignore other_id reports for now (see 8eda56033203): massive amounts of redirections to 'class' etc. makes it difficult to edit main HOL; silently ignore excessive reports -- no ambition to detect that situation accurately;

more standard names;

modernized simproc_setup; modernized theory setup;

modernized theory setup;

added simproc markup, which also indicates legacy simprocs outside the name space;

modernized simproc_setup;

misc tuning;

more contributors;

tuned;

NEWS;

tuned error -- allow user to click on hyperlink to open remote file;

no comment -- File.read_stream already enforces UTF8 (like HTML5) and HTTP servers often produce a wrong charset encoding;

improved support for external URLs, based on standard Java network operations;

basic URL operations (with Isabelle/Scala error handling);

proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);

allow text cartouches in regular outer syntax categories "text" and "altstring";

tuned comments (see Scala version);

dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;

clarifed results range;

more explicit message discrimination;

avoid confusion about pointless cursor movement with external links;

prefer regular Goal_Display.pretty_goals, without censorship of options;

more standard names;

proper context for print_tac;

more conventional tactic programming; tuned;

tuned;

reintroduce example (cf. 39281b3e4fac)

use mutual clique information (cf. c451cf8b29c8) to make N2M more robust

made N2M tactic more robust

generate cliques for 'prim(co)rec' N2M

thread mutual cliques through

generalize ln/log_powr; add log_base_powr/pow

parametricity transfer rule for INFIMUM, SUPREMUM

add divide_simps

field_simps: better support for negation and division, and power

revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules

merged

more native rm_tree, using Java 7 facilities;

expose more bad cases;

tuned signature;

more direct interpretation of "warned" status, like "failed" and independently of "finished", e.g. relevant for Rendering.overview_color of aux. files where main command status is unavailable (amending 0546e036d1c0);

simplified Text.Chunk -- eliminated ooddities; afford strict symbol_index, which is usually empty anyway;

tuned;

more frugal Symbol.Index -- no need to waste space on mostly empty arrays;

accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);

avoid data redundancy;

tuned signature -- moved Command.Chunk to Text.Chunk;

more uniform ML/document antiquotations;

obsolete;

more positions and markup;

more precise token positions;

more uniform Command.Chunk operations;

more explicit Command.Chunk types, less ooddities; tuned;

tuned;

ignore deps_changed (again) -- avoid proactive load attempts of unfinished header specification while the user is typing;

no report for position singularity, notably for aux. file, especially empty one;

simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name; more liberal hyperlink to files, allow hyperlinks within editor files independently of the (POSIX) file-system;

tuned signature -- prefer static type Document.Node.Name;

commented out example that triggers a bug

allow arguments to 'datatype_compat' in disorder

added 'datatype_compat' examples/tests

support deeply nested datatypes in 'datatype_compat'

preserve user type variable names to avoid mismatches/confusion

even more standardized doc session names after #b266e7a86485

refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;

support for URL as file name, similar to treatment in jEdit.java;

provide old-style ISABELLE_SCALA_SCRIPT for uniformity;

separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;

merged

tuned lemmas: more general class

tuned proofs;

removed abbrev "<-" again (see c771f0fe28d1) due to conflict with important "<->" and "<-->";

merged

made field_simps "more complete"

shell functions for all Isabelle executables;

renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;

more source positions;

clarified position: no offset here;

more source positions;

approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;

clarified ML bootstrap;

prepare "back" position for Navigator, before following hyperlink;

tuned;

merged

more uniform build options;

re-implemented build_doc in Isabelle/Scala; clarified command-line: specify documentation files (via document_variants) instead of sessions;

more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;

more standard hash-bang (python *is* canonical according to Admin/PLATFORMS);

tuned -- just one qualification of sections ("!");

tuned error;

proper settings instead of hard-wired information;

explicit indication of important doc sections ("!"), which are expanded in the tree view;

clarified Doc entry: more explicit path; allow plain files as Doc; refer to official jEdit documentation;

updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);

closer correspondence of document and session names, while maintaining document names for external reference

ignore jedit mark files

avoid romanism

churning pie charts (with non-canonical prerequisites!)

CONTRIBUTORS

proper inclusion into library

A single [simp] to handle the case -a/-b.

support for jEdit Navigator plugin;

more permissive Session.update_options: this is wired to jEdit PropertiesChanged, which may occur before the prover is started;

added option to Mirabelle

divide_minus_left divide_minus_right are in field_simps but are not default simprules

removing simprule status for divide_minus_left and divide_minus_right

merged;

tuned rendering -- take 1px line border into account;

revert ce37fcb30cf2 for the sake of Mac OS X -- let some event listeners of jEdit reset the cursor;

tuned white space;

use Z3 TPTP cores rather than proofs since the latter are somewhat broken

tuned spaces

merged

add missing adaptation for narrowing to work with variables of type integer => integer

merged

added ML antiquotation @{print};

afford larger full_index, to save a few milliseconds during rendering (notably text_overview);

improved parsing of "z3_tptp" proofs

merged

more direct warning within persistent Protocol.Status; consider Markup.ERROR (e.g. from Output.error_message without exception) as failure; tuned;