equal
deleted
inserted
replaced
96 val _ = |
96 val _ = |
97 (case duplicates (op =) (map fst document_variants) of |
97 (case duplicates (op =) (map fst document_variants) of |
98 [] => () |
98 [] => () |
99 | dups => error ("Duplicate document variants: " ^ commas_quote dups)); |
99 | dups => error ("Duplicate document variants: " ^ commas_quote dups)); |
100 |
100 |
|
101 val _ = writeln ("\fSession.name = " ^ name); |
101 val _ = |
102 val _ = |
102 (case Session.path () of |
103 (case Session.path () of |
103 [] => () |
104 [] => () |
104 | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path)); |
105 | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path)); |
105 val _ = |
106 val _ = |