merged

merge

fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option

updated generated files

clarified

adjusted

terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);

Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;

merged

Typo in locales tutorial.

Theory_Target.pretty: more markup;

tuned abbrevs for long arrows, according to usual ASCII syntax;

more flexibile font size via CSS <style> instead of old <font> element; preformatted text;

tuned;

control tooltip font via Swing HTML, with tooltip-font-size property;

added HTML.encode (in Scala), similar to HTML.output in ML;

one extra space to accomodate symbolic indentifiers etc.;

replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information; ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information; fall back on ML_Context.eval_text if there is no position or no surrounding text; proper Args.name_source_position for method "tactic" and "raw_tactic"; tuned;

more detailed token markup, including command kind as sub_kind; type-safe access to Command.HighlightInfo;

tuned;

separate markup for ML delimiters;

less pschedelic token markup;

simplified command/keyword markup;

markup non-identifier keyword as operator;

Isabelle_Process: do not enforce future_terminal_proof by default -- no error propagation yet;

more basic default behaviour of ENTER, HOME, END;

tuned messages;

do not highlight ignored command spans; tuned;

more explicit handling of document;

explicit markup for forked goals, as indicated by Goal.fork; accumulate pending forks within command state and hilight accordingly; Isabelle_Process: enforce future_terminal_proof, which gives some impression of non-linear/parallel checking;

avoid :\ which is not tail-recursive and tends to overflow the tiny JVM stack, which is not resizable at runtime;

define_state/new_state: provide state immediately, which is now lazy; more careful document editing: single execution future forces all entries, synchronous cancelation after update;

force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling; recovered some similarity to sequential version;

future result: retain plain Interrupt for vacuous group exceptions;

remove two examples, now that the definition of "fst" and "snd" has changed

merged

Got rid of a warning about duplicate rewrite rules.

accumulate only local results -- no proper history support yet;

avoid deprecated Iterator.fromArray;

more compiler warnings;

eliminated hard tabs;

assume given SCALA_HOME, e.g. from component settings or external setup;

merged

merged

make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work

Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes

make Nitpick "show_all" option behave less surprisingly

merged

avoid reference to thm PairE

more coherent theory structure; tuned headings

made SML/NJ quite happy;

reuse main view.font from jEdit;

deleted some old fonts;

also set font for printing, which actually works out of the box;

lib/Tools/makeall does not hardiwre logics;

discontinued Sun/Solaris tests;

some updates for release;

merged

added function update examples and set examples

updated SMT certificates