equal
deleted
inserted
replaced
220 fun encl None = enclose "[" "]" |
220 fun encl None = enclose "[" "]" |
221 | encl (Some false) = enclose "(" ")" |
221 | encl (Some false) = enclose "(" ")" |
222 | encl (Some true) = I; |
222 | encl (Some true) = I; |
223 |
223 |
224 fun file (opt_ref, path, loadit) = href_opt_path opt_ref (encl loadit (file_path path)); |
224 fun file (opt_ref, path, loadit) = href_opt_path opt_ref (encl loadit (file_path path)); |
225 val files = space_implode " + " o map file; |
225 val files = space_implode " " o map file; |
226 val parents = space_implode " + " o map (uncurry href_opt_path o apsnd name); |
226 val parents = space_implode " + " o map (uncurry href_opt_path o apsnd name); |
227 |
227 |
228 fun theory up A = |
228 fun theory up A = |
229 begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^ |
229 begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^ |
230 keyword "theory" ^ " " ^ name A ^ " = "; |
230 keyword "theory" ^ " " ^ name A ^ " = "; |