equal
deleted
inserted
replaced
387 error ("Filename \"" ^ tname ^ ".thy\" and theory name " |
387 error ("Filename \"" ^ tname ^ ".thy\" and theory name " |
388 ^ quote thy_name ^ " are different") |
388 ^ quote thy_name ^ " are different") |
389 else |
389 else |
390 (case opt_txts of |
390 (case opt_txts of |
391 Some (extxt, postxt, mltxt) => |
391 Some (extxt, postxt, mltxt) => |
392 "val base = " ^ old_thys ^ " true;\n\n\ |
392 "val thy = " ^ old_thys ^ " true;\n\n\ |
393 \structure " ^ thy_name ^ " =\n\ |
393 \structure " ^ thy_name ^ " =\n\ |
394 \struct\n\ |
394 \struct\n\ |
395 \\n\ |
395 \\n\ |
396 \local\n" |
396 \local\n" |
397 ^ trfun_defs ^ "\n\ |
397 ^ trfun_defs ^ "\n\ |
398 \in\n\ |
398 \in\n\ |
399 \\n" |
399 \\n" |
400 ^ mltxt ^ "\n\ |
400 ^ mltxt ^ "\n\ |
401 \\n\ |
401 \\n\ |
402 \val thy = base\n\n\ |
402 \val thy = thy\n\n\ |
403 \|> add_trfuns\n" |
403 \|> add_trfuns\n" |
404 ^ trfun_args ^ "\n\ |
404 ^ trfun_args ^ "\n\ |
405 \\n" |
405 \\n" |
406 ^ extxt ^ "\n\ |
406 ^ extxt ^ "\n\ |
407 \\n\ |
407 \\n\ |
411 ^ postxt ^ "\n\ |
411 ^ postxt ^ "\n\ |
412 \\n\ |
412 \\n\ |
413 \end;\n\ |
413 \end;\n\ |
414 \end;\n" |
414 \end;\n" |
415 | None => |
415 | None => |
416 "val base = " ^ old_thys ^ " false;\n\n\ |
416 "val thy = " ^ old_thys ^ " false;\n\n\ |
417 \structure " ^ thy_name ^ " =\n\ |
417 \structure " ^ thy_name ^ " =\n\ |
418 \struct\n\ |
418 \struct\n\ |
419 \\n\ |
419 \\n\ |
420 \val thy = base\n\ |
420 \val thy = thy\n\ |
421 \\n\ |
421 \\n\ |
422 \end;\n"); |
422 \end;\n"); |
423 |
423 |
424 fun theory_defn sectab tname = |
424 fun theory_defn sectab tname = |
425 header -- optional (extension sectab >> Some) None -- eof |
425 header -- optional (extension sectab >> Some) None -- eof |