Skip to content
Success

Changes

Summary

  1. suppress document_required GUI element for now: still unused;
  2. clarified layout;
  3. clarified node_required status: distinguish theory_required vs. document_required; more robust and more correct Geometry.in operation;
Changeset 76483:49acf5dd58ce by wenzelm:
suppress document_required GUI element for now: still unused;
The file was modified src/Tools/jEdit/src/theories_dockable.scala (diff)
Changeset 76482:60b963d8fc3c by wenzelm:
clarified layout;
The file was modified src/Tools/jEdit/src/theories_dockable.scala (diff)
Changeset 76481:a9d52d02bd83 by wenzelm:
clarified node_required status: distinguish theory_required vs. document_required;<br>more robust and more correct Geometry.in operation;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_model.scala (diff)
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
The file was modified src/Tools/jEdit/src/theories_dockable.scala (diff)