make compiler doubly sure;

isabelle-process: less verbose no-commit mode;

tuned message;

tuned panel names and actions;

renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;

reactivated polyml-5.4.0 -- SVN 1214 fixes a problem with arbitrary precision arithmetic that was triggered by method "approximation" in HOL/Decision_Procs/Approximation_Ex.thy;

merged

more lists lemmas

merged

merged

tuned text

sections on @{code} and code_reflect

formal syntax diagram for code_reflect

distinguish SML and Eval explicitly

no_frees_* is subsumed by new framework mechanisms in Code_Preproc

reject term variables explicitly

avoid frees and vars in terms to be evaluated by abstracting and applying

tuned whitespace

make SML/NJ happier

more conventional conversion signature

added nbe paper

continued section abut evaluation

make SML/NJ happier

new lemma

merged

new lemmas

revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms

basic setup for Session_Dockable controls;

tuned signature;

more content for Session_Dockable;

basic support for full document rendering;

Session_Dockable: basic syslog output;

just one Session.raw_messages event bus;

more reactive handling of Isabelle_Process startup errors;

eliminated Simple_Thread shorthands that can overlap with full version;

main Isabelle_Process via Isabelle_System.Managed_Process; simplified init message: no pid; misc tuning and simplification;

more robust Managed_Process.kill: check after sending signal;

more robust lib/scripts/process, with explicit script/no_script mode; added general Isabelle_System.Managed_Process, with bash_output as application; tuned;

Standard_System.with_tmp_file: deleteOnExit to make double sure;

refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;

tuned whitespace;

tuned;

added Standard_System.slurp convenience; tuned;

added Simple_Thread.future convenience; tuned;

refined ML/Scala bash wrapper, based on more general lib/scripts/process;

tuned;

more robust Isabelle_System.rm_fifo: avoid external bash invocation, which might not work in JVM shutdown phase (due to Runtime.addShutdownHook);

tuned;

added Isabelle_Process.syslog; refined Isabelle_Process.process_manager: startup_output via syslog, explicit join of auxiliary threads; tuned;

updated keywords;

merged

merged

corrected long-overlooked slip: the Pure equality of a code equation is no part of the code equation itself

dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term

Pure equality is a regular cpde operation

full palette of dynamic/static value(_strict/exn)

Factored out ML into separate file

merged

merged

remove needless exception

preprocess "Ex" before doing clausification in Metis; this is dual to "All" in b96941dddd04

expand_fun_eq -> fun_eq_iff

use buffers instead of string concatenation

renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;

more antiquotations;

added XML.content_of convenience -- cover XML.body, which is the general situation;

merged

merged

more accurate exception handling

merged

merge tracing of two related modules

merged

preprocess "All" before doing clausification in Metis; helps the definitional clausifier produce fewer clauses

reorder proof methods and take out "best"; suggestions from Tobias

renaming variable name to decrease likelyhood of nameclash

code_pred_intro can be used to name facts for the code_pred command

replacing temporary hack by checking for environment settings of the component

removing unnessary options for code_pred

moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog

removing clone in code_prolog and predicate_compile_quickcheck

adjusted

updated file duplicate

\\isatypewrite now part of isabelle latex style

made smlnj happy

properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models

do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)

generalized lemma insort_remove1 to insort_key_remove1

generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants

merged

less intermediate data structures

Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);

simplified Isabelle_System.mk_fifo: inlined script, append PPID and PID uniformly;

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)