single quote is not a valid letter any more

simple tests

boolean operators for scala

elements with start entry;

plain object;

tuned signature;

tuned;

misc tuning;

Swing_Thread.future: plain Future.value if this is already Swing;

added find_files;

pass build error code;

tuned isatest ML_OPTIONS;

merged

a primitive scala serializer

fixed type error;

remove overloaded star operator, use specific vector / matrix operators

finite annotation on cartesian product is now implicit.

added syntax translation to automatically add finite typeclass to index type of cartesian product type

Made finite cartesian products finite

reduced arity of Nitpick selectors associated with sets by 1, by using "Formula" instead of "Atom 2"

make Nitpick's tests not leave files in the temp directory

more text edit operations;

always report updates -- required has "handshake";

tuned Isabelle/Scala build;

simplified build/bootstrap of graph browser -- avoid make;

simplified build/bootstrap of Isabelle/Scala components -- avoid make;

more robust cancelation, notably of passive futures without scheduler running;

eliminated cache, which complicates the code without making a real difference (NB: deque_towards often disrupts caching, and daisy-chaining of workers already reduces queue overhead);

tasks of canceled groups are considered "ready" -- enables to purge the queue from tasks depending on unfinished promises (also improves general reactivity); shutdown: back to synchronous wait, which means no asynchronous interrupts within the loop;

do not memoize interrupts; actually memoize results in sequential version; tuned;

added Future.promise/fulfill -- promised futures that are fulfilled by external means; Future.value: official result assignment -- produces immutable ref; Future.shutdown: raw_wait keeps raw task attributes, e.g. asynchronous interrupts of toplevel; Task_Queue: passive tasks track dependencies, but lack any evaluation process; tuned;

Basic edits on plain text.

recovered legacy settings for Proof General 3.x;

merged

merged

avoid exporting Type.build_tsig

repaired legacy setting variable

merged

more correct handling of empty functions

separate module Thy_Syntax for command span parsing;

more accurate scanning of bad input;

added filter_proper parameter; added eof; added command_span;

more token discriminators;

tuned message;

tuned;

added Promise.fulfill_result;

slightly shorter tail (again) -- theory loader produces less warning spam (cf. 2524c1bbd087);

kill failed theories in reverse order -- avoids cascaded warnings;

discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);

Standard_System.raw_exec; more robust root.mkdirs;

removed function "isabelle-process", keeping "isabelle" only -- functions within the process environment might get passed through a genuine /bin/sh, which does not allow non-identifiers here;

added Cygwin "make" package;

discontinued old ISABELLE and ISATOOL environment settings;

shell functions "isabelle-process" and "isabelle" refer to the proper executables statically -- for interactive use or sloppy bash scripts;

removed further remains of mutable theory data (cf. 25bd3ed2ac9f);

merged

code cache only persists on equal theories

moved name duplicates to end of theory; reduced warning noise

merged

modernized

added applify combinator

dropped redundant name declarations

dropped copy operation for legacy TheoryDataFun

code cache without copy; tuned

report keywords as singleton messages, control message kind via print mode;

explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);

omit useless (?) scaladoc;

added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;

after_qed: refrain from Position.setmp_thread_data, which causes duplication of results with several independent proof attempts;

discontinued special HOL_USEDIR_OPTIONS;

updated stats;

made SML/NJ happy;

merged

removed legacy asm_lr_simp_tac

removed more asm_rl's - unfortunately slowdown of 1 min.

new year's resolution: reindented code in function package

provide simp and induct rules in Function.info

more official data record Function.info

simplified

absorb structures Decompose and Descent into Termination, to simplify further restructuring

another legacy "asm_lr"

merged

removed legacy asm_lr

merged

added lemmas

added lemma

removed FIXME

tuned error handling;

Standard_System.raw_execute: optional cwd; basic Cygwin.setup with download and unattended installation;

Download URLs -- with progress monitor.

Future values -- Scala version.

added simple dialogs;

added is_ready;

simplified init message -- removed redundant session property;

removed obsolete version check -- sanity delegated to Isabelle_System; tuned;

eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id; eliminated ML interface of Isar_Document: the protocol only works with certain transaction positions, i.e. via Isar commands;

tuned signature;

less ambitious isatest for SML/NJ;

killed a few warnings

more regular axiom of infinity, with no (indirect) reference to overloaded constants

back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;

removed slightly odd Isar_Document.init; simplified begin_document: associate empty command/state with no_id, which is implicit start; replaced make_id by create_id (cf. Scala version); eliminated CRITICAL/Unsynchronized.ref in favour of Synchronized.var; tuned;

explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;

tuned;

crude Cygwin.setup;

ignore undefined environment;

separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);

tuned;

system shutdown hook: strict kill;

moved Library.decode_permissive_utf8 to Isabelle_System; moved Library.with_tmp_file to Isabelle_System; added Isabelle_System.read_file/write_file; added Isabelle_System.system_out, with propagation of thread interrupts and process shutdown (global CTRL-C);

pid without newline -- required for Scala version of system_out;

higher-order treatment of temporary files;

isabelle_tool: apply platform_path only once; tuned;

slightly more paranoid cleanup of process (cf. http://kylecartmell.com/?p=9 "Five Common java.lang.Process Pitfalls");

some sanity checks for symbol interpretation;

allow UTF-8 in theory and file names;

factored-out Library.decode_permissive_utf8;

read header by scanning/parsing file;

quoted_content: handle escapes;

scan: operate on file (via Scan.byte_reader), more robust exception handling;