Skip to content
Success

Changes

Summary

  1. merged
  2. more errors;
  3. clarified inversion of file name to theory name, notably for Windows;
  4. clarified import_name: observe directory notation more strictly;
  5. tuned signature;
  6. clarified signature -- removed pointless operations;
  7. clarified signature -- removed unused content;
  8. clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
  9. find theories via session directories only -- ignore known_theories;
  10. tuned;
  11. tuned message;
  12. merged
  13. tuned
  14. A little-known material, and some tidying up
Changeset 70720:99e24569cc1f by wenzelm:
merged
Changeset 70719:b3f61e166763 by wenzelm:
more errors;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 70718:5bb025e24224 by wenzelm:
clarified inversion of file name to theory name, notably for Windows;
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_resources.scala (diff)
Changeset 70717:cceb10dcc9f9 by wenzelm:
clarified import_name: observe directory notation more strictly;
The file was modified src/Pure/PIDE/resources.ML (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
Changeset 70716:a8afe8eb3529 by wenzelm:
tuned signature;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_resources.scala (diff)
Changeset 70715:fb94d68314fa by wenzelm:
clarified signature -- removed pointless operations;
The file was modified src/Pure/PIDE/protocol.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_resources.scala (diff)
Changeset 70714:530b575d8cff by wenzelm:
clarified signature -- removed unused content;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 70713:fd188463066e by wenzelm:
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Pure/Thy/thy_header.scala (diff)
Changeset 70712:a3cfe859d915 by wenzelm:
find theories via session directories only -- ignore known_theories;
The file was modified src/Pure/ML/ml_process.scala (diff)
The file was modified src/Pure/PIDE/protocol.ML (diff)
The file was modified src/Pure/PIDE/protocol.scala (diff)
The file was modified src/Pure/PIDE/resources.ML (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.ML (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 70711:91319c3d2841 by wenzelm:
tuned;
The file was modified src/Pure/Thy/thy_info.ML (diff)
Changeset 70710:3f557ed88fd6 by wenzelm:
tuned message;
The file was modified src/Pure/PIDE/headless.scala (diff)
Changeset 70709:a95446297373 by nipkow:
merged
Changeset 70708:3e11f35496b3 by nipkow:
tuned
The file was modified src/HOL/Data_Structures/RBT_Map.thy (diff)
The file was modified src/HOL/Data_Structures/RBT_Set.thy (diff)
The file was modified src/HOL/Data_Structures/Set2_Join_RBT.thy (diff)
Changeset 70707:125705f5965f by paulson _lp15@cam.ac.uk_:
A little-known material, and some tidying up
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Complex_Analysis_Basics.thy (diff)
The file was modified src/HOL/Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy (diff)
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Complex.thy (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)