499 |
499 |
500 fun ml_val txt = "fn _ => (" ^ txt ^ ");"; |
500 fun ml_val txt = "fn _ => (" ^ txt ^ ");"; |
501 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;"; |
501 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;"; |
502 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;" |
502 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;" |
503 |
503 |
504 fun output_ml ml src ctxt txt = |
504 fun output_ml ml src ctxt (txt, pos) = |
505 (ML_Context.use_mltext (ml txt) false (SOME (Context.Proof ctxt)); |
505 (ML_Context.use_mltext false pos (ml txt) (SOME (Context.Proof ctxt)); |
506 (if ! source then str_of_source src else txt) |
506 (if ! source then str_of_source src else txt) |
507 |> (if ! quotes then quote else I) |
507 |> (if ! quotes then quote else I) |
508 |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
508 |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
509 else |
509 else |
510 split_lines |
510 split_lines |
529 ("goals", output_goals true), |
529 ("goals", output_goals true), |
530 ("subgoals", output_goals false), |
530 ("subgoals", output_goals false), |
531 ("prf", args Attrib.thms (output (pretty_prf false))), |
531 ("prf", args Attrib.thms (output (pretty_prf false))), |
532 ("full_prf", args Attrib.thms (output (pretty_prf true))), |
532 ("full_prf", args Attrib.thms (output (pretty_prf true))), |
533 ("theory", args (Scan.lift Args.name) (output pretty_theory)), |
533 ("theory", args (Scan.lift Args.name) (output pretty_theory)), |
534 ("ML", args (Scan.lift Args.name) (output_ml ml_val)), |
534 ("ML", args (Scan.lift (Args.position Args.name)) (output_ml ml_val)), |
535 ("ML_type", args (Scan.lift Args.name) (output_ml ml_type)), |
535 ("ML_type", args (Scan.lift (Args.position Args.name)) (output_ml ml_type)), |
536 ("ML_struct", args (Scan.lift Args.name) (output_ml ml_struct))]; |
536 ("ML_struct", args (Scan.lift (Args.position Args.name)) (output_ml ml_struct))]; |
537 |
537 |
538 end; |
538 end; |