--- a/src/Pure/Tools/update_cartouches.scala Thu Sep 13 16:30:07 2018 +0200
+++ b/src/Pure/Tools/update_cartouches.scala Thu Sep 13 21:18:43 2018 +0200
@@ -104,6 +104,6 @@
for {
spec <- specs
file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
- } update_cartouches(replace_text, Path.explode(File.standard_path(file)))
+ } update_cartouches(replace_text, File.path(file))
})
}
--- a/src/Pure/Tools/update_comments.scala Thu Sep 13 16:30:07 2018 +0200
+++ b/src/Pure/Tools/update_comments.scala Thu Sep 13 21:18:43 2018 +0200
@@ -63,6 +63,6 @@
for {
spec <- specs
file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
- } update_comments(Path.explode(File.standard_path(file)))
+ } update_comments(File.path(file))
})
}
--- a/src/Pure/Tools/update_header.scala Thu Sep 13 16:30:07 2018 +0200
+++ b/src/Pure/Tools/update_header.scala Thu Sep 13 21:18:43 2018 +0200
@@ -56,6 +56,6 @@
for {
spec <- specs
file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
- } update_header(section, Path.explode(File.standard_path(file)))
+ } update_header(section, File.path(file))
})
}
--- a/src/Pure/Tools/update_then.scala Thu Sep 13 16:30:07 2018 +0200
+++ b/src/Pure/Tools/update_then.scala Thu Sep 13 21:18:43 2018 +0200
@@ -50,6 +50,6 @@
for {
spec <- specs
file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
- } update_then(Path.explode(File.standard_path(file)))
+ } update_then(File.path(file))
})
}
--- a/src/Pure/Tools/update_theorems.scala Thu Sep 13 16:30:07 2018 +0200
+++ b/src/Pure/Tools/update_theorems.scala Thu Sep 13 21:18:43 2018 +0200
@@ -52,6 +52,6 @@
for {
spec <- specs
file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
- } update_theorems(Path.explode(File.standard_path(file)))
+ } update_theorems(File.path(file))
})
}