isabelle: Graph

updated examples due to changes in the way SMT certificates are stored
2010-02-02, by boehmes
merged
2010-02-02, by berghofe
merged
2010-01-31, by berghofe
Adapted to changes in cases method.
2010-01-30, by berghofe
Adapted to changes in setup of cases method.
2010-01-30, by berghofe
Added setup for simplification of equality constraints in cases rules.
2010-01-30, by berghofe
Added infrastructure for simplifying equality constraints in cases rules.
2010-01-30, by berghofe
Added "constraints" tag / attribute for specifying the number of equality
2010-01-30, by berghofe
updated SMT certificates
2010-02-02, by boehmes
updated SMT examples
2010-02-02, by boehmes
collect certificates in a single file
2010-02-02, by boehmes
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2010-02-02, by blanchet
Removed explicit type annotations
2010-02-01, by himmelma
adjusted to changes in List_Set.thy
2010-01-31, by haftmann
more correspondence lemmas between related operations
2010-01-31, by haftmann
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
2010-01-31, by haftmann
dropped some redundancies
2010-01-31, by haftmann
generalized lemma foldl_apply_inv to foldl_apply
2010-01-31, by haftmann
more correspondence lemmas between related operations; tuned some proofs
2010-01-31, by haftmann
new theory Algebras.thy for generic algebraic structures
2010-01-28, by haftmann
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
2010-01-28, by haftmann
merged
2010-01-27, by haftmann
a more complex record expression -- cf. src/HOL/Tools/quickcheck_generators.ML
2010-01-27, by haftmann
lemma Image_closed_trancl
2010-01-27, by haftmann
corrected type of typecopy constructor
2010-01-27, by haftmann
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
2010-01-27, by haftmann
Changed author; removed debugging code.
2010-01-27, by berghofe
merged
2010-01-25, by bulwahn
adding Mutabelle to repository
2010-01-25, by bulwahn
Replaced vec1 and dest_vec1 by abbreviation.
2010-01-25, by hoelzl
merged
2010-01-22, by haftmann
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
2010-01-22, by haftmann
merged
2010-01-22, by boehmes
support skolem constant for extensional arrays in Z3 proofs
2010-01-22, by boehmes
drop underscores at end of names coming from Boogie
2010-01-22, by boehmes
merged
2010-01-22, by bulwahn
correctly hiding facts of Lazy_Sequence
2010-01-22, by bulwahn
corrected and simplified Spec_Rules registration in the Recdef package
2010-01-21, by bulwahn
merged
2010-01-21, by bulwahn
adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps
2010-01-21, by bulwahn
adopting Sequences
2010-01-20, by bulwahn
added registration of equational theorems from prim_rec and rec_def to Spec_Rules
2010-01-20, by bulwahn
merged
2010-01-20, by bulwahn
function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations
2010-01-18, by krauss
merged
2010-01-20, by bulwahn
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
2010-01-20, by bulwahn
simplified proofs
2010-01-22, by haftmann
NEWS
2010-01-22, by haftmann
more accurate dependencies
2010-01-22, by haftmann
code literals: distinguish numeral classes by different entries
2010-01-22, by haftmann
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
2010-01-22, by haftmann
merged
2010-01-21, by haftmann
dropped some old primrecs and some constdefs
2010-01-16, by haftmann
explicit CONST in translations
2010-01-16, by haftmann
modernized syntax
2010-01-16, by haftmann
fix issues with previous Nitpick change
2010-01-20, by blanchet
merged
2010-01-20, by blanchet
some work on Nitpick's support for quotient types;
2010-01-20, by blanchet
removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
2010-01-14, by blanchet
Added transpose_rectangle, when the input list is rectangular.
2010-01-19, by hoelzl
Add transpose to the List-theory.
2010-01-19, by hoelzl
some examples for basic context operations;
2010-02-02, by wenzelm
minimal tuning of this slightly dated material;
2010-02-02, by wenzelm
added Subgoal.FOCUS;
2010-02-02, by wenzelm
misc tuning and clarification;
2010-02-02, by wenzelm
moved examples to proper place;
2010-02-02, by wenzelm
more details on long names, binding/naming, name space;
2010-02-01, by wenzelm
Variable.names_of;
2010-01-31, by wenzelm
more details on Isabelle symbols;
2010-01-31, by wenzelm
theory data example;
2010-01-29, by wenzelm
basic setup for ML examples: tag "mlex";
2010-01-29, by wenzelm
tuned signature;
2010-01-28, by wenzelm
formal markup of type aliases;
2010-01-28, by wenzelm
make underscores visually appear as such, although TeX-nically they are just rules (e.g. cannot be searched);
2010-01-28, by wenzelm
Netbeans Library "Scala-compiler";
2010-01-16, by wenzelm
union is an abbreviation for sup.
2010-01-15, by berghofe
merged
2010-01-15, by berghofe
Eliminated is_open option of Rule_Cases.make_nested/make_common;
2010-01-15, by berghofe
Adapted to changes in induct method.
2010-01-10, by berghofe
Adapted to changes in setup of induct method.
2010-01-10, by berghofe
Expand proofs of induct_atomize'/rulify'.
2010-01-10, by berghofe
Changed case names of converse_rtranclp_induct.
2010-01-10, by berghofe
Injectivity / distinctness theorems are now used to simplify induction rules.
2010-01-10, by berghofe
same_append_eq / append_same_eq are now used for simplifying induction rules.
2010-01-10, by berghofe
Tuned some proofs; nicer case names for some of the induction / cases rules.
2010-01-10, by berghofe
Added setup for simplification of equality constraints in induction rules.
2010-01-10, by berghofe
Added infrastructure for simplifying equality constraints.
2010-01-10, by berghofe
spurious proof failure
2010-01-15, by haftmann
merged
2010-01-14, by haftmann
merged
2010-01-14, by haftmann
dropped unused binding
2010-01-14, by haftmann
dedicated conversions to and from Int
2010-01-14, by haftmann
printing of cases
2010-01-14, by haftmann
tuned for products vs. tupled functions
2010-01-14, by haftmann
added Scala setup
2010-01-14, by haftmann
allow individual printing of numerals during code serialization
2010-01-14, by haftmann
reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)
2010-01-14, by blanchet
adjusted to changes in code equation administration
2010-01-14, by haftmann
explicit abstract type of code certificates
2010-01-13, by haftmann
corrected error messages; tuned
2010-01-13, by haftmann
function transformer preprocessor applies to both code generators
2010-01-13, by haftmann
merged
2010-01-13, by haftmann
code certificates as integral part of code generation
2010-01-12, by haftmann
import of antiquote_setup not necessary
2010-01-13, by haftmann
merged
2010-01-13, by haftmann
being more accurate wrt. list syntax
2010-01-13, by haftmann
deactivate pretty code test for Scala -- no proper setup yet
2010-01-13, by haftmann
some syntax setup for Scala
2010-01-13, by haftmann
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
2010-01-13, by wenzelm
merged
2010-01-12, by wenzelm
Parsing errors during proof reconstruction now give rise to an intelligible error message.
2010-01-12, by paulson
rebuilt from fresh copy of Bitstream Vera, for improved quality of regular text glyphs;
2010-01-12, by wenzelm
tuned initial properties/perspective;
2010-01-12, by wenzelm
provide JEDIT_SETTINGS via settings;
2010-01-12, by wenzelm
updated version and dependencies;
2010-01-12, by wenzelm
recovered subscript (cf. ded5b770ec1c);
2010-01-12, by wenzelm
formal antiquotations for ML snippets; no "open" unsynchronized references
2010-01-12, by haftmann
clarified terminology;
2010-01-11, by wenzelm
merged
2010-01-11, by wenzelm
added code certificates
2010-01-11, by haftmann
tuned code equations
2010-01-11, by haftmann
Matrices form a semiring with 0
2010-01-11, by hoelzl
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
2010-01-11, by wenzelm
ignore some src/Tools/jEdit stuff;
2010-01-11, by wenzelm
merged with converted/relocated copy of http://isabelle.in.tum.de/repos/isabelle-jedit/rev/93d884afa74b
2010-01-11, by wenzelm
more timing;
2010-01-11, by wenzelm
more tobust treatment of Document.current_state;
2010-01-11, by wenzelm
new unparsed span for text right after existing command;
2010-01-11, by wenzelm
Outer_Lex.is_ignored;
2010-01-11, by wenzelm
simplified Text_Edit;
2010-01-11, by wenzelm
eliminated strange mutable var commands;
2010-01-11, by wenzelm
updated header;
2010-01-11, by wenzelm
eliminated obsolete isabelle.proofdocument.Token;
2010-01-11, by wenzelm
do not override Command.hashCode -- which was inconsistent with eq anyway;
2010-01-11, by wenzelm
renamed Command.content to source;
2010-01-11, by wenzelm
further tuning of command_start;
2010-01-10, by wenzelm
refrain from poking blink rate -- might get stuck in invisible state;
2010-01-10, by wenzelm
eliminated Command.stop, which tends to case duplicate traversal of commands;
2010-01-10, by wenzelm
iterators for ranges of commands/starts -- avoid extra array per document;
2010-01-10, by wenzelm
tuned document changes;
2010-01-10, by wenzelm
misc tuning and clarification of Document/Change;
2010-01-10, by wenzelm
adhoc reset of blink rate;
2010-01-10, by wenzelm
provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
2010-01-10, by wenzelm
redirect scala.Console output during interpretation;
2010-01-09, by wenzelm
bind "session";
2010-01-09, by wenzelm
export isabelle_system, e.g. for use via "session" in Isabelle/Scala interpreter;
2010-01-09, by wenzelm
removed unused var plugin;
2010-01-09, by wenzelm
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
2010-01-09, by wenzelm
provide some bindings of jEdit values;
2010-01-09, by wenzelm
more precise prompt etc.;
2010-01-08, by wenzelm
define scala.home, for more robust startup of Scala tools, notably the compiler;
2010-01-08, by wenzelm
added jEdit Console and Scala compiler;
2010-01-08, by wenzelm
some attempts at Scala console plugin;
2010-01-08, by wenzelm
more precise treatment of document/state assigment;
2010-01-06, by wenzelm
more precise notion of bad messages;
2010-01-05, by wenzelm
use Text_Edit provided by Isabelle;
2010-01-05, by wenzelm
result.is_ready is not bad;
2010-01-05, by wenzelm
singleton status messages, with more precise patterns -- report bad messages;
2010-01-04, by wenzelm
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
2010-01-04, by wenzelm
slightly more uniform/robust handling of visible document;
2010-01-04, by wenzelm
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
2010-01-03, by wenzelm
more explicit treatment of command/document state;
2010-01-03, by wenzelm
removed unused document_change bus;
2010-01-03, by wenzelm
tuned;
2010-01-01, by wenzelm
tuned;
2010-01-01, by wenzelm
misc tuning;
2010-01-01, by wenzelm
tuned Change: eliminated redundant copy of document id;
2010-01-01, by wenzelm
eliminated redundant session documents database;
2010-01-01, by wenzelm
use isabelle.Future;
2010-01-01, by wenzelm
renamed current_document to recent_document (might be a bit older than current_change);
2010-01-01, by wenzelm
renamed Proof_Document to Document;
2010-01-01, by wenzelm
tuned dialog;
2009-12-31, by wenzelm
improved dialog;
2009-12-31, by wenzelm
basic setup for synchronous / modal (!) prover startup;
2009-12-31, by wenzelm
tuned signature;
2009-12-30, by wenzelm
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
2009-12-30, by wenzelm
tuned signature of isabelle.Position;
2009-12-30, by wenzelm
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
2009-12-30, by wenzelm
unified Command and Command_State, eliminated separate Accumulator;
2009-12-30, by wenzelm
removed experimental history panel;
2009-12-30, by wenzelm
more explicit modeling of Command and Command_State as Session.Entity;
2009-12-30, by wenzelm
updated;
2009-12-30, by wenzelm
tuned;
2009-12-29, by wenzelm
tuned caret_listener/selected_command;
2009-12-29, by wenzelm
misc tuning;
2009-12-29, by wenzelm
eliminated global Session.document_0 -- did not work due to hardwired id;
2009-12-29, by wenzelm
tuned;
2009-12-29, by wenzelm
tuned;
2009-12-29, by wenzelm
Standard_System;
2009-12-28, by wenzelm
slightly larger stack size -- default seems to be as low as 256k;
2009-12-23, by wenzelm
back to activate=startup (again) -- ensure that Isabelle_Encoding refers to valid Isabelle.system;
2009-12-23, by wenzelm
adapted to class Outer_Syntax;
2009-12-22, by wenzelm
renamed session.info to session.root;
2009-12-22, by wenzelm
tuned;
2009-12-22, by wenzelm
just one variable for outer syntax keywords and completion;
2009-12-22, by wenzelm
added isabelle-session mode for session.info files;
2009-12-21, by wenzelm
tuned keywords;
2009-12-21, by wenzelm
sort completions by plain string order;
2009-12-21, by wenzelm
cache results;
2009-12-18, by wenzelm
imitate PG 4 colors;
2009-12-18, by wenzelm
tuned;
2009-12-18, by wenzelm
simplified Isabelle_Process.Result;
2009-12-17, by wenzelm
explicit object Session.Global_Settings;
2009-12-16, by wenzelm
actually use JEDIT_JAVA_OPTIONS from settings, not ..._ARGS;
2009-12-16, by wenzelm
some explicit Swing_Thread guards;
2009-12-15, by wenzelm
direct apply for Document_Model and Document_View;
2009-12-15, by wenzelm
need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED;
2009-12-15, by wenzelm
merged
2009-12-15, by wenzelm
Cobra version;
2009-12-15, by wenzelm
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
2009-12-15, by wenzelm
clarified BufferListener: use adapter, listen to contentInserted instead of preContentInserted;
2009-12-15, by wenzelm
refined treatment of default logic concerning property and GUI;
2009-12-15, by wenzelm
handle "default" logic;
2009-12-11, by wenzelm
more serious command line handling;
2009-12-11, by wenzelm
proper uninstall;
2009-12-11, by wenzelm
removed unused Session.prover_logic;
2009-12-11, by wenzelm
class Session models full session, with or without prover process (cf. heaps, browser_info);
2009-12-10, by wenzelm
tuned;
2009-12-10, by wenzelm
basic setup for HTML_Panel event handling;
2009-12-10, by wenzelm
install_fonts;
2009-12-10, by wenzelm
renamed "raw output" to "protocol";
2009-12-08, by wenzelm
proper actor wiring for raw process output;
2009-12-08, by wenzelm
misc tuning;
2009-12-08, by wenzelm
prefer options from running application;
2009-12-08, by wenzelm
more precise messages;
2009-12-08, by wenzelm
back to low-level JPanel, required for addNotify/removeNotify;
2009-12-08, by wenzelm
added properties_changed event bus;
2009-12-08, by wenzelm
provide dummy URL;
2009-12-08, by wenzelm
generic HTML_Panel -- specific Results_Dockable;
2009-12-08, by wenzelm
tuned;
2009-12-08, by wenzelm
tuned;
2009-12-08, by wenzelm
simplified register_fonts;
2009-12-08, by wenzelm
tuned library names;
2009-12-08, by wenzelm
misc modernization of names;
2009-12-08, by wenzelm
misc rearrangement of files;
2009-12-08, by wenzelm
removed remains of Flying Saucer;
2009-12-08, by wenzelm
manipulate document within Swing thread only -- potentially slow;
2009-12-08, by wenzelm
tuned JVM settings;
2009-12-08, by wenzelm
misc updates;
2009-12-07, by wenzelm
obsolete;
2009-12-07, by wenzelm
use IsabelleText by default;
2009-12-07, by wenzelm
misc updates;
2009-12-07, by wenzelm
simplified treatment of Isabelle fonts, via Isabelle_System.register_fonts (requires Java 1.6);
2009-12-07, by wenzelm
removed ScrollerDockable, which is based on discontinued Flying Saucer renderer;
2009-12-07, by wenzelm
use IsabelleText font;
2009-12-07, by wenzelm
reduced logging;
2009-12-06, by wenzelm
tuned message markup;
2009-12-04, by wenzelm
plain results, no markup here;
2009-12-04, by wenzelm
basic setup for Cobra HTML renderer;
2009-12-04, by wenzelm
results: XML.Tree;
2009-12-04, by wenzelm
basic platform update;
2009-11-14, by wenzelm
Prover: private Actor;
2009-09-17, by wenzelm
tuned;
2009-09-16, by wenzelm
misc tuning;
2009-09-16, by wenzelm
Linear_Set.append_after;
2009-09-16, by wenzelm
tuned file name;
2009-09-15, by wenzelm
tuned file name;
2009-09-15, by wenzelm
renamed PhaseOverviewPanel to Document_Overview;
2009-09-15, by wenzelm
tooltip: HTML dummy;
2009-09-15, by wenzelm
tuned;
2009-09-15, by wenzelm
misc tuning and unification;
2009-09-15, by wenzelm
refrain from actor shutdown -- slightly low-level;
2009-09-15, by wenzelm
keep BufferListener and TextAreaExtension private;
2009-09-15, by wenzelm
tuned white space;
2009-09-15, by wenzelm
misc tuning;
2009-09-15, by wenzelm
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
2009-09-15, by wenzelm
single instance of rule_set;
2009-09-15, by wenzelm
regular activate=defer -- may debug remotely, no need to run under netbeans;
2009-09-13, by wenzelm
avoid fractional font metrics, which produces bad antialiasing with reletively new versions of jedit and java;
2009-09-13, by wenzelm
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
2009-09-08, by wenzelm
tuned;
2009-09-07, by wenzelm
tuned;
2009-09-07, by wenzelm
Prover: just one actor -- single message dispatch;
2009-09-07, by wenzelm
modernized Event_Bus -- based on actors;
2009-09-07, by wenzelm
eliminated ProverEvents.Activate -- handle "ready" within Prover;
2009-09-07, by wenzelm
corrected order
2009-09-07, by immler
sidekick root data: set buffer length to avoid crash of initial caret move;
2009-09-06, by wenzelm
tuned color (PG 4.0);
2009-09-06, by wenzelm
treat all messages except status as results;
2009-09-06, by wenzelm
tuned;
2009-09-06, by wenzelm
tuned;
2009-09-06, by wenzelm
replaced find_command_at by command_at -- null-free, proper Option;
2009-09-06, by wenzelm
tuned;
2009-09-06, by wenzelm
tuned;
2009-09-06, by wenzelm
minor tuning;
2009-09-06, by wenzelm
tuned MarkupNode argument order;
2009-09-05, by wenzelm
eliminated MarkupInfo, moved particular variants into object Command;
2009-09-05, by wenzelm
removed dead code;
2009-09-05, by wenzelm
MarkupNode: removed id;
2009-09-05, by wenzelm
simplified MarkupNode -- independent of Command and ProofDocument;
2009-09-04, by wenzelm
minor tuning;
2009-09-04, by wenzelm
sorted;
2009-09-03, by wenzelm
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
2009-09-03, by wenzelm
tuned imports;
2009-09-03, by wenzelm
tuned;
2009-09-03, by wenzelm
tuned;
2009-09-03, by wenzelm
State: immutable;
2009-09-03, by wenzelm
tuned;
2009-09-03, by wenzelm
minor tuning;
2009-09-03, by wenzelm
unified Swing_Thread.delay_first/last;
2009-09-02, by wenzelm
sealed Edit;
2009-09-02, by wenzelm
Isabelle_Process: receiver as Actor -- requires Scheduler.shutdown in the end;
2009-09-01, by wenzelm
option -d: enable debugger;
2009-09-01, by wenzelm
modernized Isar_Document;
2009-09-01, by wenzelm
use Linear_Set from Isabelle/Pure.jar;
2009-09-01, by wenzelm
lazy fields
2009-08-27, by immler
better performance
2009-08-27, by immler
no busy waiting
2009-08-27, by immler
global event buses for changes concerning commands and document edits
2009-08-27, by immler
include scala-swing
2009-08-27, by immler
merged
2009-08-27, by immler
must unapply edits in reverse order
2009-08-27, by immler
fixed some issues with multiple active buffers
2009-08-27, by immler
clarified structure of TheoryView
2009-08-27, by immler
improved repainting
2009-08-27, by immler
tuned whitespace
2009-08-27, by immler
catching NPE on val
2009-08-27, by immler
Command and Command_State handle results from prover as Accumulator
2009-08-27, by immler
trait Accumulator;
2009-08-27, by immler
Command notifies changes
2009-08-27, by immler
change_receiver and output_info are used before regular initialisation
2009-08-27, by immler
TheoryView starts Prover
2009-08-27, by immler
output_info specific to prover
2009-08-27, by immler
proper activation with multiple buffers
2009-08-27, by immler
state_update global in Plugin
2009-08-27, by immler
unused
2009-08-27, by immler
fixed special case;
2009-08-27, by immler
added shortcut
2009-08-27, by immler
generalized settings;
2009-08-22, by wenzelm
Isabelle component;
2009-08-22, by wenzelm
less ambitious array operations -- for improved compatibility with older versions of bash;
2009-08-22, by wenzelm
Text is not present any more
2009-08-13, by immler
typo
2009-08-13, by immler
Change consisting of a list of Edits
2009-08-07, by immler
add is a private function
2009-08-03, by immler
avoid internal "add" method;
2009-07-27, by wenzelm
removed unused imports;
2009-07-27, by wenzelm
decode offsets with respect to symbols
2009-07-15, by immler
equal should be included
2009-07-15, by immler
arbitrary history
2009-07-13, by immler
commands carrying state-information
2009-07-08, by immler
gui element to set current document version
2009-07-08, by immler
set current document version; forget "future" versions in list
2009-07-08, by immler
current version in theoryview/buffer
2009-07-08, by immler
activation
2009-07-08, by immler
remember removed text
2009-07-08, by immler
insert mode isabelle into catalog
2009-07-08, by immler
updated to jedit 4.3pre17 -- no longer provide separate ml.xml;
2009-07-05, by wenzelm
updated to jEdit 4.3pre17;
2009-07-05, by wenzelm
removed obsolete isabelle.utils.Delay;
2009-07-05, by wenzelm
renamed Delay to clarified version Swing_Thread.delay;
2009-07-04, by wenzelm
change_receiver: removed redundant Swing_Thread wrapper -- the Delay timer action is already in Swing;
2009-07-04, by wenzelm
replaced utils.Delay by tune version isabelle.Delay (Pure.jar);
2009-07-04, by wenzelm
use symbolic NULL;
2009-07-04, by wenzelm
tuned token styles, according to some earlier Isabelle/jEdit experiments;
2009-07-04, by wenzelm
use static Map/Set for token categorization;
2009-07-04, by wenzelm
added symbol_index (presently unused);
2009-07-04, by wenzelm
misc tuning;
2009-07-04, by wenzelm
updated to Netbeans 6.7;
2009-07-03, by wenzelm
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
2009-06-30, by wenzelm
preload CSS resources;
2009-06-27, by wenzelm
more robust handling of Isabelle CSS files;
2009-06-26, by wenzelm
default file is plain Scratch.thy (as in Proof General);
2009-06-26, by wenzelm
removed obsolete VFS -- superceded by IsabelleEncoding;
2009-06-26, by wenzelm
prover.set_document: plain name, no path for now;
2009-06-26, by wenzelm
removes VFS service -- superceded by UTF-8-Isabelle encoding;
2009-06-26, by wenzelm
recovered Isabelle font -- deriveFont(Int) refers to style, not size!
2009-06-26, by wenzelm
opt-out obscure encodings;
2009-06-26, by wenzelm
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
2009-06-26, by wenzelm
decentralized Isabelle component names;
2009-06-26, by wenzelm
renamed UTF-8-isabelle to UTF-8-Isabelle;
2009-06-26, by wenzelm
pass JVM platform files, without going through the "isabelle:" VFS;
2009-06-26, by wenzelm
more precise wrapping of I/O streams;
2009-06-26, by wenzelm
some support for actual symbol recoding;
2009-06-25, by wenzelm
added IsabelleEncoding -- a clone of utf-8 for now;
2009-06-25, by wenzelm
added Boolean_Property, Int_Property;
2009-06-25, by wenzelm
simplified option pane: proper logic title, hardwired font path;
2009-06-25, by wenzelm
_canonPath: expand_path;
2009-06-25, by wenzelm
renamed IsabelleProcess to Isabelle_Process;
2009-06-25, by wenzelm
misc tuning and reorganization;
2009-06-25, by wenzelm
default sidekick.complete-delay;
2009-06-23, by wenzelm
fall back on Isabelle system completion (symbols only);
2009-06-23, by wenzelm
use isabelle.Completion;
2009-06-23, by wenzelm
acces position properties via Isabelle library;
2009-06-18, by wenzelm
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
2009-06-17, by wenzelm
basic keyword completions via isabelle.Scan.Lexicon;
2009-06-17, by wenzelm
minor tuning;
2009-06-16, by wenzelm
updated notes about Isabelle environment, no longer need to use "isabelle env netbeans";
2009-06-07, by wenzelm
static IsabelleSystem.charset (cf. http://isabelle.in.tum.de/repos/isabelle/rev/be0f7f4f9e12);
2009-06-07, by wenzelm
automated update by Scala plugin 6.7v1;
2009-06-04, by wenzelm
produce ids via Isabelle.system (http://isabelle.in.tum.de/repos/isabelle/rev/c23663825e23);
2009-06-04, by wenzelm
ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
2009-06-04, by wenzelm
more robust get_offsets;
2009-06-04, by wenzelm
updates for Netbeans 6.7;
2009-06-03, by wenzelm
merged
2009-06-02, by wenzelm
merged
2009-06-02, by immler
merged; resolved superficial conflicts
2009-06-02, by immler
linearset works faster here
2009-06-02, by immler
lists work faster here
2009-06-02, by immler
fixed duplicate document-id
2009-06-02, by immler
ignore unchanged commands
2009-06-02, by immler
ignore unchanged tokens
2009-06-02, by immler
split change on activate
2009-06-02, by immler
return unchanged node on errors
2009-06-02, by immler
handle_result: activate via explicit status "ready" (cf. http://isabelle.in.tum.de/repos/isabelle/rev/ce169bd37fc0);
2009-06-02, by wenzelm
superficial tuning;
2009-06-02, by wenzelm
updated versions;
2009-06-02, by wenzelm
type_at: no quotes;
2009-06-02, by wenzelm
tuned;
2009-06-02, by wenzelm
use RichString.* to produce blanks;
2009-06-02, by wenzelm
change_receiver: start only once (already done in actor function);
2009-06-02, by wenzelm
superficial tuning;
2009-06-02, by wenzelm
slightly more robust treatment of options via arrays;
2009-05-30, by wenzelm
merged
2009-05-30, by wenzelm
outer syntax could clash with status on removed commands
2009-05-27, by immler
no null change
2009-05-27, by immler
fixed delete markup
2009-05-27, by immler
check presence of begin, end in attributes
2009-05-27, by immler
treat comments like seperate commands,
2009-05-27, by immler
split large changes for faster responses of prover
2009-05-27, by immler
changed handling of subdirectories
2009-05-25, by immler
more accurate setup for "jEdit" project;
2009-05-30, by wenzelm
recovered iso-latin-1 text;
2009-05-23, by wenzelm
improved handling of markup-information with command=null
2009-05-22, by immler
implemented links to other files
2009-05-22, by immler
implemented IsabelleHyperlinkSource (only links inside the current buffer)
2009-05-22, by immler
corrected offset
2009-05-22, by immler
fixed duplicate activation
2009-05-22, by immler
removed debug-painting
2009-05-22, by immler
let MarkupNode carry arbitrary information
2009-05-22, by immler
added hyperlink plugin
2009-05-22, by immler
ML types in tooltip
2009-05-22, by immler
chaned '+'
2009-05-22, by immler
reduced to one markup-tree
2009-05-22, by immler
implemented filter on markup-tree
2009-05-22, by immler
fixed flatten
2009-05-22, by immler
immutable markup-nodes;
2009-04-29, by immler
seperate node for syntax-highlighting
2009-04-27, by immler
included information on ML status messages in Sidekick's status-window
2009-04-27, by immler
abs. stops, markup nodes depend on doc-version;
2009-04-22, by immler
merged
2009-04-20, by immler
Anti-aliasing is now controlled via the smoothing threshhold
2009-04-20, by immler
incomplete changes of immutable tokens and commands
2009-04-20, by immler
prepared proofdocument for only needed changes
2009-04-16, by immler
use jEdits styles
2009-04-15, by immler
corrected displaying of phases in buffer with few lines;
2009-04-15, by immler
fixed shifting;
2009-04-14, by immler
correct order, added curreeeent change
2009-04-07, by immler
implemented to_current and from_current in dependancy of document-versions
2009-04-06, by immler
proofdocument-versions get id from changes
2009-04-06, by immler
when jEdit is run from Netbeans, activate=defer does not work (why?)
2009-03-28, by immler
merged: resolved conflicts with Markups: ML-syntax styles in styles.props
2009-03-23, by immler
changes of text with unique id
2009-03-20, by immler
fixes
2009-03-20, by immler
merged; resolved conflicts (kept own versions)
2009-03-19, by immler
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
2009-03-19, by immler
build jar before running/debugging
2009-03-19, by immler
probably setup from new Scala Plugin 0.15.1 for NetBeans
2009-03-19, by immler
LinearSet.prev
2009-03-19, by immler
merged, resolving minor conflicts;
2009-03-02, by wenzelm
preliminary/failed attempt to use the new IsarDocument access model to the prover;
2009-03-02, by wenzelm
ProofDocument without state
2009-03-08, by immler
*very* superficial usage of LinearSet
2009-03-05, by immler
implemented delete_after
2009-03-05, by immler
implemented insert_after
2009-03-05, by immler
changed title
2009-03-04, by immler
added Makarius' LinearSet
2009-03-04, by immler
tokens and commands as lists
2009-02-19, by immler
styles properties
2009-02-05, by immler
syntax styles in properties
2009-02-04, by immler
all token kinds have to be non-null
2009-02-04, by immler
removed redundant code
2009-02-04, by immler
added ML syntax markup;
2009-03-20, by wenzelm
recovered activate=defer, which is the "new" way to invoke jEdit plugins (cf. 3fbb7b565013);
2009-03-20, by wenzelm
more robust copying of jars;
2009-03-20, by wenzelm
referred to old version of TokenMarker
2009-02-02, by immler
implemented markTokens;
2009-02-02, by immler
more flexible commands-iterators
2009-02-01, by immler
use FontMetrics.getMaxAdvance if available; tuned
2009-02-01, by immler
renamed fields of MarkupNode; implemented flatten and leafs
2009-02-01, by immler