renamed Plugin.plugin to Plugin.self; use Plugin.self.symbols; tuned;

renamed Plugin.plugin to Plugin.self; tuned Plugin.font handling;

renamed Plugin.plugin to Plugin.self; added Symbol.Interpretation (formerly in VFS); tuned Plugin.font handling; tuned;

renamed Plugin.plugin to Plugin.self;

tuned;

renamed isabelle.jedit.UserAgent to isabelle.renderer.UserAgent;

tuned;

basic setup of anti-aliasing, according to jEdit property; tuned;

tuned order of menu items;

renamed isabelle.prover.IsabelleSKParser to isabelle.jedit.IsabelleSideKickParser; tuned;

tuned sidekick properties;

setPreferredSize for floating dockables;

default docking of sidekick and isabelle-state;

more conventional action names;

added author field; adapted isabelle action names; tuned;

regular plugin activation via "defer"; enable sidekick for "isabelle" and "ml" mode, not "text"; tuned;

basic isabelle mode setup;

renamed IsabellePlugin to Isabelle; tuned properties according to http://isabelle.in.tum.de/repos/isabelle/file/b1c6f4563df7/lib/jedit/plugin/Isabelle.props;

misc tuning and adaption according to original IsabelleParser -- cf. http://isabelle.in.tum.de/repos/isabelle/file/b1c6f4563df7/lib/jedit/plugin/isabelle_parser.scala;

obsolete, cf. build.xml and makedist;

MOVABLE="TRUE" reuses existing instance when changing docking position -- cf. http://www.jedit.org/api/org/gjt/sp/jedit/gui/DockableWindowManager.html

updated to 4.3pre16;

removed jEdit sources from target;

more robust handling of FILES with spaces, using bash array variables;

disabled tracing;

misc tuning;

proper spelling of JEDIT_JAVA_OPTIONS; no extra quoting of FILES;

added some headers and comments;

added some headers and comments;

restructured: independent provers in different buffers

added 'delay or ignore'

delayed repainting new phase in buffer and overview; reverted johannes' handling of removed Commands

information on command-phase left of scrollbar (with panel)

information on command-phase left of scrollbar

structure of markup-tree in scala, keep track of swing-nodes in background

MarkupNode instead of DefaultMutableTreeNode and RelativeAsset

interpretation of STATUS messages in one place, deleting inner syntax

no syserr

handle statuses in Command

command property: offset relative to start of command

include Sidekick its dependency ErrorList in dist

removed debugging output

basic tree structure for sidekick

encoloring only details in the current line!

ugly fine-grained buffer markup

Token-functions with type-parameters

moved methods to object Token

arbitrary type for tokens

removed xsymbol converting -> sidekick should do that

revalidate for repainting

merge

adj scrolling

abstract buffers and renderer

use build-nb.xml for "debug" as well;

basic setup for auxiliary project "jEdit", with full sources, debugging, profiling;

updated version of nbproject, as produced by build in Netbeans 6.5;

adapted jar locations;

incorporated NOTES into TODO;

updates for Netbeans 6.5;

pass results to Scroller

replacing xsymbols *after* inserting text

buffer as array

convert eg pasted xsymbols

removed System.err...

copy-paste for XHTMLPanels

register to buffer all messages

done

fine grained scrolling

removed senseless lines

restructured scroller

renamed to message_panel

playing with xsymbols

use utf-8 charset encoding

copying selection to clipboard

selecting text of state view

worked over autoscrolling

removed imports

minimum height for panels, immediate scrolling and correct waiting

scroll to first message immediately; potential later messages periodically

auto-scrolling

prepared for automatic scrolling

cleaned up a bit, scrolling arbitrary heights (incremental rendering)

UserAgent as seperate class, moved stylesheets, baseURL to UserAgent

using 'dist' directory for jEdit-settings => find Isabelle-plugin directly

fine scrolling principally possible

calculate preferred sizes only when needed

renamed class

renamed

reverted and ignoring build.xml

faster resizing, unlimited caching(but cache is cleared on resize)

reverted build.xml

absolute positioning according to preferred size of panels, scrolling one message per unit rendered messages are cached

correct resizing of xhtml-panels

LazyScroller: rendering messages only when needed - very basic functionallity

a version of Dixon's ML mode with less ambitious indentation;

Misc development notes.

added jvmpath conversion for Cygwin;

hint on -settings=...;

renamed VFS protocol prefix from "isa:" to "isabelle:";

explicit home path for default file -- more robust; pass -settings=... here, not via Isabelle settings -- more robust;

disabled tracing;

essential default properties for jEdit;

Isabelle/jEdit interface wrapper.

make Isabelle/jEdit distribution;

refined application.args;

reading command_decls from 'new' protocol

added target -pre-jar which copies jEdit plugin to be included in jar;

added application.args (Why does it end up in pricate properties?);

tuned whitespace;

fixed jEdit version;

requires Java from Sun; hints on running;

Requirements to build from sources.

removed private properties;

basic setup for running jEdit;

deactivated tests due to lack of testng installation;

basic Netbeans project setup;

explicit result type for _listFiles;

original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;

tuned message;

clarified Symbol.is_plain/is_wellformed -- is_closed was rejecting plain backslashes;

Text_Edit.toString;

timeit message;

treat *all* JVM throwables as "exceptions", cf. ML version;

simplified Text_Edit -- deflated class hierarchy;

Outer_Lex.is_ignored;

merged

merged

proper types for user-defined syntax

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;

added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);

removed unused read_file;

tidied proofs

made sml/nj happy

updated certificates

updated example

merged verification condition structure and term representation in one datatype, extended the set of operations on verification conditions (retrieve more information, advanced splitting of paths), simplified discharging of verification conditions (due to improved datatype), added variantions of commands (extract different parts of verification conditions, scan until first "hard" assertion)

merged

updated generated document sources

take care for destructive print mode properly using dedicated pretty builders

merged

made sml/nj happy

merged

dropped junk

reduced code generator cache to the baremost minimum

updated documentation

updated generated examples

reduced code generator cache to the baremost minimum; corrected spelling

basic setup for header scanning/parsing;

clarified atom parser: return content; added tags parser;

tuned;

renamed class Outer_Keyword to Outer_Syntax; renamed tokenize to scan (cf. ML version);

Isabelle session manager -- most basic setup;

actually closer file reader;

tuned;

added plain read_file;

consider proper input only; added wrappers;

added completion -- lazy avoids excessive table building; tuned signature;

Generic parsers for Isabelle/Isar outer syntax -- Scala version.

class Outer_Keyword wraps symbol interpretation, lexicon, keyword table;

explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure; added Token_Reader; tuned;

Changes in generated code, apparently caused by changes to the code generation system itself.

Polishing up the English

merged

merged

clarified various user-defined syntax issues

prefer prefix "iso" over potentially misleading "is"; tuned

moved lemmas o_eq_dest, o_eq_elim here

add 'morphisms' option to domain_isomorphism command

merged

generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs

rename equals_zero_I to minus_unique (keep old name too)

add lemma swap_triple

improve performance by reordering of parser combinators;

added nested comments; tuned;

more Scala sources;

simiplified result of keyword parser (again); sort completions by plain string order; moved Reverse to library.scala;

simplified result of keyword and symbols parser; some support for parsing outer syntax tokens;

Outer lexical syntax for Isabelle/Isar -- Scala version.

refined some Symbol operations/signatures; tuned;

refined some Symbol operations/signatures; added Symbol.Matcher; flexible Scan.Lexicon.symbols, with one/many/many1 variants;

added basic library -- Scala version; added extra support for exceptions -- Scala version; moved exn.ML to accompany exn.scala;

indicate final state of keywords; added symbol scanner;

added symbol classification; tuned;

tuned;

merged

imitate PG style;

merged

imitate PG colors;

made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default; up to now, only Auto Quickcheck did -- the old behavior is available by passing "no_assms" as option

merged

polished Nitpick's binary integer support etc.; etc. = improve inconsistent scope correction + sort values nicely in output + handle "mod" using the characterization "x mod y = x - x div y * y" (instead of explicit code in Nitpick) + introduce KK = Kodkod as abbreviation

merged

added support for binary nat/int representation to Nitpick

distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick; this improves Nitpick's precision in some cases (e.g. higher-order constructors) and reflects a better understanding of what's going on

merged

get rid of polymorphic equality in Nitpick's code + a few minor cleanups

added "no_assms" option to Refute, and include structured proof assumptions by default; will do the same for Quickcheck unless there are objections

markup bad YXML as malformed; removed unused XML.document; removed unused markup;

replace invalid code points -- instead of exception;

tuned signature;

removed junk (cf. f49d45afa634);

merged

merged

add lemma INFM_conjI

added lemmas about INFM/MOST

add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff

add lemmas open_image_fst, open_image_snd

Result.cache;

cache for partial sharing;

merged

Two new theorems about cardinality

replace 'UNIV - S' with '- S'

re-state lemmas using 'range'

make proof use only abstract properties of eventually

swap_self already declared [simp]

declare swap_self [simp], add lemma comp_swap

fifo: raw byte stream; Result: fully decoded symbols and tree structure; adapted to simplified message format; tuned;

added decode_chars, with raw character view on byte buffer and adhoc decoding via toString; parse/chunks: avoid direct string comparison, to make it actually work with abstract CharSequence;

tuned signature;

tuned;

simplified message format: chunks with explicit size in bytes; robust message header via YXML.binary_text; standard_message: refer to thread position only; discontinued obsolete "-" output stream; tuned;

robust representation of low ASCII control characters within XML/YXML text;

merged

filter out identical completions;

spaces not allowed, unfortunately

user aliasses

merged

replaced blast by metis (blast hangs with polyml-5.2)

avoid negative indices as argument ot drop

Upgraded a warning to an error

merged

improved crude deriving_show inference

explicit name for function space

make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits

make Nitpick "Core" test more conservative, to avoid problems on Larry's machine

made sml/nj happy

also sort verification conditions before printing

print assertions in a more natural order

removed unique ids -- now in session.scala;

merged

Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution; tuned;

Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;

merged

repaired accident: do not forget module contents if there are no imports

option width for Code_Target.code_of

default_code_width is now proper theory data

merged

updated dependencies

make assertion labels unique already when loading a verification condition, keep abstract view on verification conditions and provide various splitting operations on verification conditions, allow to discharge only parts of a verification condition, extended the command "boogie_vc" with options to consider only some assertions or to split a verification condition into its paths, added a narrowing option to "boogie_status" (a divide-and-conquer approach for identifying the "hard" subset of assertions of a verification conditions), added tactics "boogie", "boogie_all" and "boogie_cases", dropped tactic "split_vc", split example Boogie_Max into Boogie_Max (proof based on SMT) and Boogie_Max_Stepwise (proof based on metis and auto with documentation of the available Boogie commands), dropped (mostly unused) abbreviations

depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)

merged

moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)

avoid dependency on implicit dest rule predicate1D in proofs

merged

NEWS

merged

merged

take and drop as projections of chop

explicit lower bound for index

merged

merged

streamlined proofs

fixed typo

merged

only invoke metisFT if metis failed

added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas

merged

each import resides in its own line

using existing lattice classes

added get_data;

sealed XML.Tree; keep original XML.Tree within DOM as user data;

simplified Cygwin setup, assuming 1.7 registry layout (version 1.5 suffers from upcaseenv problem anyway);

slightly more robust and less ambitious version of install_fonts;

more robust Cygwin.config: actually check Wow6432Node, prefer explicit CYGWIN_ROOT in any case;

merged

merged

merged

made Nitpick work also for people who import "Plain" instead of "Main"

make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes

keep future Isabelle application entry point;

merged

also consider the fully-typed version of metis for Mirabelle measurements

merged

made SML/NJ happy

simplified notion of empty module name

commit

resorted code equations from "old" number theory version

merged

split off evaluation mechanisms in separte module Code_Eval

register_fonts: more precise error handling;

added future;

depend on Java 1.6 after all;

basic support for IsabelleText fonts;

merged

merged

tuned inner structure

merged Crude_Executable_Set into Executable_Set

merged

avoid using "prop_logic.ML" and "sat_solver.ML" twice (the other occurrence being in "FunDef.thy"); this produces two copies of the same module, with separate references etc.

better error message in Refute when specifying a non-existing SAT solver

merged

updated certificate

merged

repaired read_const_expr, broken in 1e7ca47c6c3d

merged

verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)

faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization), custom-made (top-down) atomize_conv, store predicate and function symbols in a table instead of a list for faster lookup, updated certificates

merged

tuned proofs

tuned lattices theory fragements; generlized some lemmas from sets to lattices

avoid lazy val with side-effects -- spurious null pointers!?

toString: more robust handling of null; tuned;

proper markup text for loc;

output_syms: permissive treatment of control symbols, cf. Scala version;

basic treatment of special control symbols; misc tuning;

elements: more convenient result;

more robust treatment of line breaks -- Java "split" has off semantics;

added auxiliary constructors;

added elements: Interator; first isHighSurrogate, not isLowSurrogate; misc tuning and generalization;

merged

merged

tuned whitespace

merged, resolving minor conflicts

NEWS

signatures for generated code; tuned

tuned

avoid misleading name "superarities"

more speaking function names for Code_Printer; added doublesemicolon

tuned code setup

version of IsabelleMono that retains plain ASCII and ISO-LATIN-1 from Bitstream Vera;

output linefeed as </br> -- workaround problem with <pre> in Lobo Browser 0.98.4; output_width: uniform mapping -- avoid obscure fastpath optimization;

added markup for hidden text; handle "\<^bold>" as markup; HTML output: include original control symbols as hidden text, to enable copy-paste;

Basic HTML output.

output "'" as "&#39;" which is a bit more portable ("&apos;" is defined in XML/XHTML, but not in old-style HTML4);

fixed paths in Nitpick's ML file headers

added soundness fix to Nitpick's history

export symbols from Minipick (so I can use them in other programs)

make proof work again

fix soundness bug in Nitpick's "destroy_constrs" optimization

merged, resolving minor conflict, and recovering sane state;

merged

merged

merged, resolving minor conflicts;

merged

merged

modernized structure Datatype_Aux

tuned

dropped some unused bindings

modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML

more accurate linerarity

merged

Inl and Inr now with authentic syntax

renamed former datatype.ML to datatype_data.ML

renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML

modernized; dropped ancient constant Part

centralized sum type matter in Sum_Type.thy

tuned

bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)

merged

normalized uncurry take/drop

merged