equal
deleted
inserted
replaced
108 val m = length ths; |
108 val m = length ths; |
109 val j = i + m; |
109 val j = i + m; |
110 in |
110 in |
111 if a <> "" then ((a, ths), j) |
111 if a <> "" then ((a, ths), j) |
112 else if m = n then ((name, ths), j) |
112 else if m = n then ((name, ths), j) |
113 else if m = 1 then |
113 else ((Facts.string_of_ref (Facts.Named ((name, Position.none), |
114 ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.Single i])), ths), j) |
114 SOME ([if m = 1 then Facts.Single i else Facts.FromTo (i, j - 1)]))), ths), j) |
115 else |
|
116 ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.FromTo (i, j - 1)])), ths), j) |
|
117 end; |
115 end; |
118 in fst (fold_map name_res res 1) end; |
116 in fst (fold_map name_res res 1) end; |
119 |
117 |
120 in |
118 in |
121 |
119 |