use_text/use_file now depend on explicit ML name space;
authorwenzelm
Wed Sep 17 23:44:31 2008 +0200 (2008-09-17)
changeset 282842161665a0a5d
parent 28283 dbe9c820e4d2
child 28285 91cd65eabd7f
use_text/use_file now depend on explicit ML name space;
Admin/isatest/annomaly.ML
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/Admin/isatest/annomaly.ML	Wed Sep 17 23:23:49 2008 +0200
     1.2 +++ b/Admin/isatest/annomaly.ML	Wed Sep 17 23:44:31 2008 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4  
     1.5  in
     1.6  
     1.7 -  fun use_text tune str_of_pos (line, name) p v t =
     1.8 +  fun use_text tune str_of_pos name_space (line, name) p v t =
     1.9      let val name = case name of "" => "unnamed" | name => name
    1.10          val arcs = rewrite ["use_text"] name
    1.11          (* should we have different files for different line numbers? *
    1.12 @@ -55,12 +55,12 @@
    1.13  		      andalso name = "ML"
    1.14  		   then ["empty_Isabelle", "empty" ] else arcs
    1.15          val _    = AnnoMaLy.nameNextStream arcs
    1.16 -    in  smlnj_use_text tune str_of_pos (line, name) p v t  end;
    1.17 +    in  smlnj_use_text tune str_of_pos name_space (line, name) p v t  end;
    1.18  
    1.19 -  fun use_file tune str_of_pos output verbose name =
    1.20 +  fun use_file tune str_of_pos name_space output verbose name =
    1.21        let val arcs = rewrite ["use_file"] name
    1.22            val _    = AnnoMaLy.nameNextStream arcs
    1.23 -      in  smlnj_use_file tune str_of_pos output verbose name  end;
    1.24 +      in  smlnj_use_file tune str_of_pos name_space output verbose name  end;
    1.25  
    1.26    fun forget_structure name =
    1.27        let val arcs = [ "forget_structure", name ]
     2.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Sep 17 23:23:49 2008 +0200
     2.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Sep 17 23:44:31 2008 +0200
     2.3 @@ -138,7 +138,7 @@
     2.4    in use_text tune str_of_pos name_space (1, name) output verbose txt end;
     2.5  
     2.6  fun forget_structure name =
     2.7 -  use_text (fn x => x) (fn _ => "") (1, "ML") (TextIO.print, fn s => raise Fail s) false
     2.8 +  use_text (fn x => x) (fn _ => "") () (1, "ML") (TextIO.print, fn s => raise Fail s) false
     2.9      ("structure " ^ name ^ " = struct end");
    2.10  
    2.11