Changes

Summary

merged
access Isabelle theory exports via virtual file-system;
clarified signature;
clarified output (again);
more operations;
tuned signature;
tuned
tuned headers
clarified output;
tuned;
export generated files;
clarified Path.check_elem;

Changeset 69638:938b28a99863 by wenzelm: merged
Changeset 69637:f3b564a13236 by wenzelm: access Isabelle theory exports via virtual file-system;
The file was added	`src/Tools/jEdit/src/isabelle_export.scala`
The file was modified	`src/Tools/jEdit/lib/Tools/jedit` (diff)
The file was modified	`src/Tools/jEdit/src/services.xml` (diff)
Changeset 69636:dd1e0e1570d2 by wenzelm: clarified signature;
The file was modified	`src/Tools/jEdit/src/jedit_lib.scala` (diff)
The file was modified	`src/Tools/jEdit/src/plugin.scala` (diff)
Changeset 69635:95dc926fa39c by wenzelm: clarified output (again);
The file was modified	`src/Pure/Thy/export.scala` (diff)
Changeset 69634:70f1994988d4 by wenzelm: more operations;
The file was modified	`src/Pure/PIDE/command.scala` (diff)
The file was modified	`src/Pure/Thy/export.scala` (diff)
Changeset 69633:3d91a7a58113 by wenzelm: tuned signature;
The file was modified	`src/Pure/PIDE/document.scala` (diff)
Changeset 69632:7d02b7bee660 by nipkow: tuned
The file was modified	`src/HOL/Analysis/Ordered_Euclidean_Space.thy` (diff)
Changeset 69631:6c3e6038e74c by nipkow: tuned headers
The file was modified	`src/HOL/Analysis/Derivative.thy` (diff)
The file was modified	`src/HOL/Analysis/Finite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Ordered_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Tagged_Division.thy` (diff)
Changeset 69630:aaa0b5f571e8 by wenzelm: clarified output;
The file was modified	`src/Pure/Thy/export.scala` (diff)
Changeset 69629:e1188d9d616b by wenzelm: tuned;
The file was modified	`src/Pure/Thy/export.scala` (diff)
Changeset 69628:a2fbfdc5e62d by wenzelm: export generated files;
The file was modified	`src/Pure/Tools/generated_files.ML` (diff)
The file was modified	`src/Tools/Haskell/Haskell.thy` (diff)
Changeset 69627:3e26471d6d01 by wenzelm: clarified Path.check_elem;
The file was modified	`src/Pure/General/path.ML` (diff)
The file was modified	`src/Pure/Thy/export.ML` (diff)