equal
deleted
inserted
replaced
34 else if kind = "exception" |
34 else if kind = "exception" |
35 then txt1 ^ " of " ^ txt2 |
35 then txt1 ^ " of " ^ txt2 |
36 else txt1 ^ ": " ^ txt2; |
36 else txt1 ^ ": " ^ txt2; |
37 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
37 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
38 val _ = writeln (ml (txt1, txt2)); |
38 val _ = writeln (ml (txt1, txt2)); |
39 val _ = ML_Context.use_mltext false Position.none (ml (txt1, txt2)) (SOME (Context.Proof ctxt)); |
39 val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2)); |
40 in |
40 in |
41 "\\indexml" ^ kind ^ enclose "{" "}" |
41 "\\indexml" ^ kind ^ enclose "{" "}" |
42 (translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c) txt1) ^ |
42 (translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c) txt1) ^ |
43 ((if ! O.source then str_of_source src else txt') |
43 ((if ! O.source then str_of_source src else txt') |
44 |> (if ! O.quotes then quote else I) |
44 |> (if ! O.quotes then quote else I) |