src/Tools/jEdit/src/prover/Prover.scala
2009-09-06 wenzelm 2009-09-06 minor tuning;
2009-09-04 wenzelm 2009-09-04 minor tuning;
2009-09-01 wenzelm 2009-09-01 Isabelle_Process: receiver as Actor -- requires Scheduler.shutdown in the end; handle_message: plain function Isabelle_Process.parse_message avoids race on process variable in the first place;
2009-09-01 wenzelm 2009-09-01 modernized Isar_Document;
2009-08-27 immler 2009-08-27 global event buses for changes concerning commands and document edits
2009-08-27 immler 2009-08-27 catching NPE on val
2009-08-27 immler 2009-08-27 Command and Command_State handle results from prover as Accumulator accumulating results in State; prover outputs any result
2009-08-27 immler 2009-08-27 Command notifies changes
2009-08-27 immler 2009-08-27 change_receiver and output_info are used before regular initialisation
2009-08-27 immler 2009-08-27 TheoryView starts Prover
2009-08-27 immler 2009-08-27 output_info specific to prover
2009-08-07 immler 2009-08-07 Change consisting of a list of Edits
2009-07-13 immler 2009-07-13 arbitrary history
2009-07-08 immler 2009-07-08 commands carrying state-information
2009-07-08 immler 2009-07-08 current version in theoryview/buffer
2009-07-08 immler 2009-07-08 activation
2009-06-30 wenzelm 2009-06-30 renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
2009-06-25 wenzelm 2009-06-25 renamed IsabelleProcess to Isabelle_Process; renamed IsabelleSystem to Isabelle_System;
2009-06-23 wenzelm 2009-06-23 fall back on Isabelle system completion (symbols only); tuned;
2009-06-23 wenzelm 2009-06-23 use isabelle.Completion;
2009-06-18 wenzelm 2009-06-18 acces position properties via Isabelle library;
2009-06-17 wenzelm 2009-06-17 basic keyword completions via isabelle.Scan.Lexicon;
2009-06-04 wenzelm 2009-06-04 more robust get_offsets; set_document: removed obsolete dummy command;
2009-06-02 wenzelm 2009-06-02 handle_result: activate via explicit status "ready" (cf. http://isabelle.in.tum.de/repos/isabelle/rev/ce169bd37fc0); tuned;
2009-06-02 wenzelm 2009-06-02 superficial tuning;
2009-05-27 immler 2009-05-27 outer syntax could clash with status on removed commands
2009-05-27 immler 2009-05-27 no null change
2009-05-27 immler 2009-05-27 check presence of begin, end in attributes
2009-05-22 immler 2009-05-22 improved handling of markup-information with command=null
2009-05-22 immler 2009-05-22 implemented IsabelleHyperlinkSource (only links inside the current buffer)
2009-05-22 immler 2009-05-22 let MarkupNode carry arbitrary information
2009-05-22 immler 2009-05-22 reduced to one markup-tree
2009-04-29 immler 2009-04-29 immutable markup-nodes; more seperate nodes in command; restructured handling of markups in prover
2009-04-27 immler 2009-04-27 seperate node for syntax-highlighting
2009-04-27 immler 2009-04-27 included information on ML status messages in Sidekick's status-window
2009-04-22 immler 2009-04-22 abs. stops, markup nodes depend on doc-version; fixed missing positions in ProofDocument.text_changed; relink only changed commands in ProofDocument.token_changed
2009-04-06 immler 2009-04-06 proofdocument-versions get id from changes
2009-03-20 immler 2009-03-20 fixes
2009-03-19 immler 2009-03-19 merged; resolved conflicts (kept own versions)
2009-03-19 immler 2009-03-19 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
2009-03-02 wenzelm 2009-03-02 preliminary/failed attempt to use the new IsarDocument access model to the prover; misc tuning;
2009-03-08 immler 2009-03-08 ProofDocument without state handle text-events via actor
2009-02-19 immler 2009-02-19 tokens and commands as lists
2009-01-27 wenzelm 2009-01-27 eliminated Command.Status.REMOVE/REMOVED; support rudiments of new document protocol: running flag, edits/edit message; use plain toInt; misc tuning and rearrangement;
2009-01-27 wenzelm 2009-01-27 ProofDocument: pass is_command_keyword directly, not via full-blown Prover object;
2009-01-27 wenzelm 2009-01-27 eliminated Prover.start -- part of main constructor;
2009-01-27 wenzelm 2009-01-27 tuned whitespace;
2009-01-27 wenzelm 2009-01-27 beginnings of global document state;
2009-01-27 wenzelm 2009-01-27 misc tuning;
2009-01-27 wenzelm 2009-01-27 Prover.start: determine logic in one place;
2009-01-27 wenzelm 2009-01-27 more explicit indication of mutable collections;
2009-01-20 wenzelm 2009-01-20 misc tuning -- de-camelization;
2009-01-20 wenzelm 2009-01-20 Command: turned content into plain val;
2009-01-20 wenzelm 2009-01-20 use Symbol.Interpretation from IsabelleSystem instance;
2009-01-20 wenzelm 2009-01-20 replaced java.util.Property by plain association list; handle_result: do not parse ignored messages; tuned;
2009-01-19 wenzelm 2009-01-19 joined Document with ProofDocument; misc tuning;
2009-01-19 wenzelm 2009-01-19 superficial tuning;
2009-01-16 wenzelm 2009-01-16 IsabelleProcess.parse_message (message markup within Scala layer);
2009-01-12 immler 2009-01-12 implemented IsabelleSideKickParser.complete removed Plugin.prover (to avoid NoSuchElementException)
2009-01-11 wenzelm 2009-01-11 decl_info: cover both commands and keywords, with kind; command_decls: maintain kinds as well (Map);