equal
deleted
inserted
replaced
505 fun ml_val txt = "fn _ => (" ^ txt ^ ");"; |
505 fun ml_val txt = "fn _ => (" ^ txt ^ ");"; |
506 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;"; |
506 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;"; |
507 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;" |
507 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;" |
508 |
508 |
509 fun output_ml ml src ctxt (txt, pos) = |
509 fun output_ml ml src ctxt (txt, pos) = |
510 (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos (ml txt); |
510 (ML_Context.eval_in (SOME ctxt) false pos (ml txt); |
511 (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos))) |
511 (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos))) |
512 |> (if ! quotes then quote else I) |
512 |> (if ! quotes then quote else I) |
513 |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
513 |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
514 else |
514 else |
515 split_lines |
515 split_lines |