tuned;
authorwenzelm
Thu Sep 13 21:18:43 2018 +0200 (2 months ago)
changeset 68994d961e11e0e87
parent 68991 6c1beb52d766
child 68995 10da16970d82
tuned;
src/Pure/Tools/update_cartouches.scala
src/Pure/Tools/update_comments.scala
src/Pure/Tools/update_header.scala
src/Pure/Tools/update_then.scala
src/Pure/Tools/update_theorems.scala
     1.1 --- a/src/Pure/Tools/update_cartouches.scala	Thu Sep 13 16:30:07 2018 +0200
     1.2 +++ b/src/Pure/Tools/update_cartouches.scala	Thu Sep 13 21:18:43 2018 +0200
     1.3 @@ -104,6 +104,6 @@
     1.4        for {
     1.5          spec <- specs
     1.6          file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
     1.7 -      } update_cartouches(replace_text, Path.explode(File.standard_path(file)))
     1.8 +      } update_cartouches(replace_text, File.path(file))
     1.9      })
    1.10  }
     2.1 --- a/src/Pure/Tools/update_comments.scala	Thu Sep 13 16:30:07 2018 +0200
     2.2 +++ b/src/Pure/Tools/update_comments.scala	Thu Sep 13 21:18:43 2018 +0200
     2.3 @@ -63,6 +63,6 @@
     2.4        for {
     2.5          spec <- specs
     2.6          file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
     2.7 -      } update_comments(Path.explode(File.standard_path(file)))
     2.8 +      } update_comments(File.path(file))
     2.9      })
    2.10  }
     3.1 --- a/src/Pure/Tools/update_header.scala	Thu Sep 13 16:30:07 2018 +0200
     3.2 +++ b/src/Pure/Tools/update_header.scala	Thu Sep 13 21:18:43 2018 +0200
     3.3 @@ -56,6 +56,6 @@
     3.4        for {
     3.5          spec <- specs
     3.6          file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
     3.7 -      } update_header(section, Path.explode(File.standard_path(file)))
     3.8 +      } update_header(section, File.path(file))
     3.9      })
    3.10  }
     4.1 --- a/src/Pure/Tools/update_then.scala	Thu Sep 13 16:30:07 2018 +0200
     4.2 +++ b/src/Pure/Tools/update_then.scala	Thu Sep 13 21:18:43 2018 +0200
     4.3 @@ -50,6 +50,6 @@
     4.4        for {
     4.5          spec <- specs
     4.6          file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
     4.7 -      } update_then(Path.explode(File.standard_path(file)))
     4.8 +      } update_then(File.path(file))
     4.9      })
    4.10  }
     5.1 --- a/src/Pure/Tools/update_theorems.scala	Thu Sep 13 16:30:07 2018 +0200
     5.2 +++ b/src/Pure/Tools/update_theorems.scala	Thu Sep 13 21:18:43 2018 +0200
     5.3 @@ -52,6 +52,6 @@
     5.4      for {
     5.5        spec <- specs
     5.6        file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
     5.7 -    } update_theorems(Path.explode(File.standard_path(file)))
     5.8 +    } update_theorems(File.path(file))
     5.9    })
    5.10  }