equal
deleted
inserted
replaced
73 if kind = "type" then txt1 ^ " = " ^ txt2 |
73 if kind = "type" then txt1 ^ " = " ^ txt2 |
74 else if kind = "exception" then txt1 ^ " of " ^ txt2 |
74 else if kind = "exception" then txt1 ^ " of " ^ txt2 |
75 else txt1 ^ ": " ^ txt2; |
75 else txt1 ^ ": " ^ txt2; |
76 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
76 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
77 val _ = writeln (ml (txt1, txt2)); |
77 val _ = writeln (ml (txt1, txt2)); |
78 val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2)); |
78 val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2)); |
79 in |
79 in |
80 "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^ |
80 "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^ |
81 ((if ! O.source then str_of_source src else txt') |
81 ((if ! O.source then str_of_source src else txt') |
82 |> (if ! O.quotes then quote else I) |
82 |> (if ! O.quotes then quote else I) |
83 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
83 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |