equal
deleted
inserted
replaced
873 | prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^ |
873 | prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^ |
874 (prts pfn ps (p+1) ts) |
874 (prts pfn ps (p+1) ts) |
875 in pr_pt f [] pt end; |
875 in pr_pt f [] pt end; |
876 (* |
876 (* |
877 > fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n"; |
877 > fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n"; |
878 > val pt = ref EmptyPtree; |
878 > val pt = Unsynchronized.ref EmptyPtree; |
879 > pt:=Nd("root'", |
879 > pt:=Nd("root'", |
880 [Nd("xx1",[]), |
880 [Nd("xx1",[]), |
881 Nd("xx2", |
881 Nd("xx2", |
882 [Nd("xx2.1.",[]), |
882 [Nd("xx2.1.",[]), |
883 Nd("xx2.2.",[])]), |
883 Nd("xx2.2.",[])]), |
1062 | insert b (Nd (b', bs)) (p::ps) = |
1062 | insert b (Nd (b', bs)) (p::ps) = |
1063 Nd (b', repl_app bs p (insert b (nth p bs) ps)); |
1063 Nd (b', repl_app bs p (insert b (nth p bs) ps)); |
1064 (* |
1064 (* |
1065 > type ppobj = string; |
1065 > type ppobj = string; |
1066 > writeln (pr_ptree prfn (!pt)); |
1066 > writeln (pr_ptree prfn (!pt)); |
1067 val pt = ref Empty; |
1067 val pt = Unsynchronized.ref Empty; |
1068 pt:= insert ("root'":ppobj) EmptyPtree []; |
1068 pt:= insert ("root'":ppobj) EmptyPtree []; |
1069 pt:= insert ("xx1":ppobj) (!pt) [1]; |
1069 pt:= insert ("xx1":ppobj) (!pt) [1]; |
1070 pt:= insert ("xx2":ppobj) (!pt) [2]; |
1070 pt:= insert ("xx2":ppobj) (!pt) [2]; |
1071 pt:= insert ("xx3":ppobj) (!pt) [3]; |
1071 pt:= insert ("xx3":ppobj) (!pt) [3]; |
1072 pt:= insert ("xx2.1":ppobj) (!pt) [2,1]; |
1072 pt:= insert ("xx2.1":ppobj) (!pt) [2,1]; |