removed debug-painting

let MarkupNode carry arbitrary information

added hyperlink plugin

ML types in tooltip

chaned '+'

reduced to one markup-tree

implemented filter on markup-tree

fixed flatten

immutable markup-nodes; more seperate nodes in command; restructured handling of markups in prover

seperate node for syntax-highlighting

included information on ML status messages in Sidekick's status-window

abs. stops, markup nodes depend on doc-version; fixed missing positions in ProofDocument.text_changed; relink only changed commands in ProofDocument.token_changed

merged

Anti-aliasing is now controlled via the smoothing threshhold

incomplete changes of immutable tokens and commands

prepared proofdocument for only needed changes

use jEdits styles

corrected displaying of phases in buffer with few lines; tuned

fixed shifting; synchronized commit

correct order, added curreeeent change

implemented to_current and from_current in dependancy of document-versions

proofdocument-versions get id from changes

when jEdit is run from Netbeans, activate=defer does not work (why?)

merged: resolved conflicts with Markups: ML-syntax styles in styles.props

changes of text with unique id

fixes

merged; resolved conflicts (kept own versions)

Prover as actor managing ProofDocument-versions (removed EventBus structural_changes); added actor to TheoryView, receiving updates of Commands (removed EventBus command_info); Prover.edit_document from Makarius 'broken' repository; LinearSet: fixed prev

build jar before running/debugging

probably setup from new Scala Plugin 0.15.1 for NetBeans

LinearSet.prev

merged, resolving minor conflicts;

preliminary/failed attempt to use the new IsarDocument access model to the prover; misc tuning;

ProofDocument without state handle text-events via actor

*very* superficial usage of LinearSet

implemented delete_after

implemented insert_after

changed title

added Makarius' LinearSet

tokens and commands as lists

styles properties

syntax styles in properties

all token kinds have to be non-null

removed redundant code

added ML syntax markup;

recovered activate=defer, which is the "new" way to invoke jEdit plugins (cf. 3fbb7b565013); proper encoding for JVM property files: iso-latin-1;

more robust copying of jars;

referred to old version of TokenMarker

implemented markTokens; moved choose_color to DynamicTokenMarker and extended to choose_style

more flexible commands-iterators

use FontMetrics.getMaxAdvance if available; tuned

renamed fields of MarkupNode; implemented flatten and leafs

respect current offsets

modified netbeans build such that dist can be used as settings-directory for jedit; adapted explicit makedist

merge

take content of asset for description in status-view of Sidekick

eliminated Command.Status.REMOVE/REMOVED; support rudiments of new document protocol: running flag, edits/edit message; use plain toInt; misc tuning and rearrangement;

eliminated Command.Status.REMOVE/REMOVED; added state_id; refined add_result: running flag;

eliminated Command.Status.REMOVE/REMOVED;

use plain toInt;