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);