refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop; tuned;

back to default fold painter -- Circle looks slightly odd in conjunction with bracket matching;

message_actor: more robust treatment of EOF;

simplified Isabelle_Process message kinds; misc tuning and simplification;

recovered basic session stop/restart;

simplified fifo handling -- rm_fifo always succeeds without ever blocking; tuned;

raw_execute: let IOException pass-through unhindered (again);

mkfifo: some workaround to ensure reasonably unique id, even on Cygwin where $PPID might fall back on odd default;

Isabelle_System.mk_fifo: more robust enumeration of unique names, based on persisting JVM pid (parent of shell process);

slightly more robust Isabelle_Process startup -- NB: openening fifo streams synchronizes with other end, which may fail to reach that point;

tuned;

separate Isabelle.logic_selector;

non-editable text area;

basic setup for prover session panel;

ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;

discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);

Isabelle_Markup.overview_color: indicate error / warning messages;

some specific message classification;

Syntax.read_asts error: report token ranges within message -- no side-effect here;

Isabelle_Process: status/report do not require serial numbers;

simplified some internal flags using Config.T instead of full-blown Proof_Data;

tuned signature of (Context_)Position.report variants;

merged

merged

update README

regenerate "metis.ML"

fix license

updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)

move functions around

simplify Skolem handling; things are much easier now that Sledgehammer doesn't skolemize, only Metis

make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}

complete refactoring of Metis along the lines of Sledgehammer

got caught once again by SML's pattern maching (ctor vs. var)

added new "Metis_Reconstruct" module, temporarily empty

rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"

move SPASS's Flotter hack to "Sledgehammer_Reconstruct"

skip some "important" messages

refactoring: move ATP proof and error extraction code to "ATP_Proof" module

merged

added lemmas

merged

proper closures for static evaluation; no need for FIXMEs any longer

refined static_eval_conv_simple; tuned comments

closures preserve static serializer context for static evaluation; tuned

closures separate serializer initialization from serializer invocation as far as appropriate

add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions

made sml/nj happy

merged

added code_stmts antiquotation from doc-src/more_antiquote.ML

added output_typewriter from doc-src/more_antiquote.ML

moved material intro distribution proper

merged

merged

separation of static and dynamic thy context

adjusted setup

dynamic and static value computation; built-in evaluation of propositions

Exn.map_result

adjusted to changes in Code_Runtime

merged

merged

improving replacing higher order arguments to work with tuples

adding another context free grammar example for the predicate compiler

adding values to show and ensure that values works with complex terms and restores numerals on natural numbers

adding restoring of numerals for natural numbers for values command