equal
deleted
inserted
replaced
268 |
268 |
269 local |
269 local |
270 |
270 |
271 fun activate_target thy target = |
271 fun activate_target thy target = |
272 let |
272 let |
273 val ((targets, abortable), default_width) = Targets.get thy; |
273 val ((_, abortable), default_width) = Targets.get thy; |
274 val (modify, data) = collapse_hierarchy thy target; |
274 val (modify, data) = collapse_hierarchy thy target; |
275 in (default_width, abortable, data, modify) end; |
275 in (default_width, abortable, data, modify) end; |
276 |
276 |
277 fun activate_syntax lookup_name src_tab = Symtab.empty |
277 fun activate_syntax lookup_name src_tab = Symtab.empty |
278 |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier |
278 |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier |
628 |
628 |
629 (* concrete syntax *) |
629 (* concrete syntax *) |
630 |
630 |
631 local |
631 local |
632 |
632 |
633 fun zip_list (x::xs) f g = |
633 fun zip_list (x :: xs) f g = |
634 f |
634 f |
635 :|-- (fn y => |
635 :|-- (fn y => |
636 fold_map (fn x => g |-- f >> pair x) xs |
636 fold_map (fn x => g |-- f >> pair x) xs |
637 :|-- (fn xys => pair ((x, y) :: xys))); |
637 :|-- (fn xys => pair ((x, y) :: xys))); |
638 |
638 |