Skip to content
Success

Changes

Summary

  1. added abstract editor operations, notably for Query_Operation;
  2. tuned signature;
  3. tuned;
  4. clarified modules;
  5. clarified modules;
Changeset 66085:100f02099532 by wenzelm:
added abstract editor operations, notably for Query_Operation;
The file was modified src/Tools/VSCode/src/server.scala (diff)
Changeset 66084:7f8eeff20f7a by wenzelm:
tuned signature;
The file was modified src/Pure/PIDE/editor.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)
The file was modified src/Tools/jEdit/src/output_dockable.scala (diff)
Changeset 66083:dcc685d5c3f7 by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)
The file was modified src/Tools/jEdit/src/plugin.scala (diff)
Changeset 66082:2d12a730a380 by wenzelm:
clarified modules;
The file was modified src/Pure/PIDE/editor.scala (diff)
The file was modified src/Tools/jEdit/src/active.scala (diff)
The file was modified src/Tools/jEdit/src/debugger_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
The file was modified src/Tools/jEdit/src/document_view.scala (diff)
The file was modified src/Tools/jEdit/src/documentation_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
The file was modified src/Tools/jEdit/src/output_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/plugin.scala (diff)
The file was modified src/Tools/jEdit/src/query_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/rich_text_area.scala (diff)
The file was modified src/Tools/jEdit/src/simplifier_trace_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/sledgehammer_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/state_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/theories_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/timing_dockable.scala (diff)
Changeset 66081:441f95b05944 by wenzelm:
clarified modules;
The file was modified src/Tools/VSCode/extension/src/library.ts (diff)
The file was modified src/Tools/VSCode/extension/src/preview.ts (diff)