Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Thu, 23 Aug 2012 12:00:11 +0200
changeset 48897 873fdafc5b09
parent 48896 bb1f461a7815
child 48898 9fc880720663
tuned signature;
src/Pure/ProofGeneral/pgip_isabelle.ML file | annotate | diff | comparison | revisions
src/Pure/Thy/thy_load.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Thu Aug 23 11:58:10 2012 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Thu Aug 23 12:00:11 2012 +0200
@@ -79,7 +79,7 @@
                NONE => (NONE, NONE)
              | SOME fname =>
                let val path = Path.explode fname in
-                 if can (Thy_Load.check_file Path.current) path
+                 if File.exists path
                  then (SOME (PgipTypes.pgipurl_of_path path), NONE)
                  else (NONE, SOME fname)
                end);
--- a/src/Pure/Thy/thy_load.ML	Thu Aug 23 11:58:10 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Aug 23 12:00:11 2012 +0200
@@ -9,7 +9,6 @@
   val master_directory: theory -> Path.T
   val imports_of: theory -> string list
   val provide: Path.T * SHA1.digest -> theory -> theory
-  val check_file: Path.T -> Path.T -> Path.T
   val thy_path: Path.T -> Path.T
   val check_thy: Thy_Header.keywords -> Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, imports: string list,
isabelle