equal
deleted
inserted
replaced
97 else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1)) |
97 else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1)) |
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 _ = ML_Context.eval_in (SOME ctxt) false (#pos source1) (ml (toks1, toks2)); |
102 val _ = |
|
103 ML_Context.eval_in (SOME ctxt) {SML = false, verbose = false} (#pos source1) |
|
104 (ml (toks1, toks2)); |
103 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
105 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
104 in |
106 in |
105 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
107 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
106 (txt' |
108 (txt' |
107 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |
109 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |