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;

clarified Version.syntax -- avoid guessing initial situation;

more abstract Prover.Syntax, as proposed by Carst Tankink;

tuned signature (see also 0850d43cb355);

slightly more readable protocol trace (NB1: prover input is always marked as <prover_command/>; NB2: adding indentation would invalidate the XML);

recovered public command_line from d92eb5c3960d, which is important for alternative prover processes;

tuned rendering for 5 different look-and-feels;

more symbol abbrevs, e.g. relevant for list comprehension in HOL/List.thy or HOL/Library/Monad_Syntax.thy;

more general prover operations;

tuned signature -- pro forma;

more general prover operations;

Merge

Cleaned up some messy proofs

fix #0556204bc230

merged DERIV_intros, has_derivative_intros into derivative_intros

don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)

use Alt-Ergo 0.95.2, the latest and greatest version

updated Z3 TPTP to 4.3.1+

updated Why3 version in docs

added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes

use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges

removed clone (cf. 300f613060b0)

tuned signature -- more explicit iterator terminology;

more explicit iterator terminology, in accordance to Scala 2.8 library; clarified Graph.keys_iterator vs. Graph.keys, with subtle change of semantics; tuned output;

extend continuous_intros; remove continuous_on_intros and isCont_intros

reorder Complex_Analysis_Basics; rename DD to deriv

moved generic theorems from Complex_Analysis_Basic; fixed some theorem names

merged;

tuned rendering;

new theorem about zero limits

New theorems for extracting quotients

more contributors;

document value generation for quickcheck's testers

tuned whitespace;

suppress slightly odd completion of "simp";

observe extra line spacing for output as well;

persistent protocol_status, to improve performance of node_status a little;

more uniform painting of caret, which also improves visibility in invisible state;

tuned rendering -- visual indication of the status range, to make more clear when information might is out of view;

tuned for-comprehensions -- less structure mapping;

some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);

more direct command states -- merge_results is hardly ever needed;

unused;

more frugal command_status, which is often used in a tight loop;

simplified using "value class";

more precise BNF bound for datatypes

compile

tuning

added new-style (co)datatype interpretation hook

added BNF interpretation hook

added 'ctr_sugar' interpretation hook

tuned