src/Pure/proof_general.ML
changeset 16259 aed1a8ae4b23
parent 16022 96a9bf7ac18d
child 16440 9b6e6d5fba05
     1.1 --- a/src/Pure/proof_general.ML	Sun Jun 05 11:31:21 2005 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Sun Jun 05 11:31:22 2005 +0200
     1.3 @@ -322,20 +322,20 @@
     1.4  fun tell_file_loaded path = 
     1.5      if pgip() then
     1.6  	issue_pgipe "informtheoryloaded"  (* FIXME: get thy name from info here? *)
     1.7 -		    [thyname_attr        (XML.text (File.sysify_path path)),
     1.8 -		     localfile_url_attr  (XML.text (File.sysify_path path))]
     1.9 +		    [thyname_attr        (XML.text (File.platform_path path)),
    1.10 +		     localfile_url_attr  (XML.text (File.platform_path path))]
    1.11      else 
    1.12  	emacs_notify ("Proof General, this file is loaded: " 
    1.13 -		      ^ quote (File.sysify_path path));
    1.14 +		      ^ quote (File.platform_path path));
    1.15  
    1.16  fun tell_file_retracted path = 
    1.17      if pgip() then
    1.18  	issue_pgipe "informtheoryretracted"  (* FIXME: get thy name from info here? *)
    1.19 -		    [thyname_attr        (XML.text (File.sysify_path path)),
    1.20 -		     localfile_url_attr  (XML.text (File.sysify_path path))]
    1.21 +		    [thyname_attr        (XML.text (File.platform_path path)),
    1.22 +		     localfile_url_attr  (XML.text (File.platform_path path))]
    1.23      else 
    1.24  	emacs_notify ("Proof General, you can unlock the file " 
    1.25 -		      ^ quote (File.sysify_path path));
    1.26 +		      ^ quote (File.platform_path path));
    1.27  
    1.28  
    1.29  (* theory / proof state output *)
    1.30 @@ -1158,7 +1158,7 @@
    1.31  
    1.32    fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
    1.33        case Url.unpack url of
    1.34 -	  (Url.File path) => File.sysify_path path
    1.35 +	  (Url.File path) => File.platform_path path
    1.36  	| _ => error ("Cannot access non-local URL " ^ url)
    1.37  
    1.38    val fileurl_of = localfile_of_url o (xmlattr "url")