equal
deleted
inserted
replaced
98 then txt1 ^ ": " ^ txt2 |
98 then txt1 ^ ": " ^ txt2 |
99 else txt1 ^ " : " ^ txt2; |
99 else txt1 ^ " : " ^ txt2; |
100 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
100 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
101 |
101 |
102 val _ = |
102 val _ = |
103 ML_Context.eval_in (SOME ctxt) {SML = false, verbose = false} (#pos source1) |
103 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source1) (ml (toks1, toks2)); |
104 (ml (toks1, toks2)); |
|
105 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
104 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
106 in |
105 in |
107 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
106 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
108 (txt' |
107 (txt' |
109 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |
108 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |