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;