# HG changeset patch
# User wenzelm
# Date 1457382821 -3600
# Node ID f1baa15a6a0c1c75f9842e99107505fd12d17a1c
# Parent  9498623b27f05d664c379ea98b530efdf8be5865
tuned -- more standard operations;

diff -r 9498623b27f0 -r f1baa15a6a0c src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Mar 07 21:09:28 2016 +0100
+++ b/src/Pure/Thy/present.ML	Mon Mar 07 21:33:41 2016 +0100
@@ -35,7 +35,7 @@
 val doc_indexN = "session";
 val session_graph_path = Path.basic "session_graph.pdf";
 
-fun show_path path = Path.implode (Path.expand (Path.append (File.pwd ()) path));
+fun show_path path = Path.implode (Path.expand (File.full_path Path.current path));
 
 
 
diff -r 9498623b27f0 -r f1baa15a6a0c src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Mar 07 21:09:28 2016 +0100
+++ b/src/Tools/Code/code_target.ML	Mon Mar 07 21:33:41 2016 +0100
@@ -348,9 +348,8 @@
 fun assert_module_name "" = error "Empty module name not allowed here"
   | assert_module_name module_name = module_name;
 
-fun using_master_directory ctxt =
-  Option.map (Path.append (File.pwd ()) o
-    Path.append (Resources.master_directory (Proof_Context.theory_of ctxt)));
+val using_master_directory =
+  Option.map o File.full_path o Resources.master_directory o Proof_Context.theory_of;
 
 in