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 pos = #pos source1; |
102 val _ = |
103 val _ = |
103 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source1) (ml (toks1, toks2)); |
104 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2)) |
|
105 handle ERROR msg => error (msg ^ Position.here pos); |
104 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
106 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
105 in |
107 in |
106 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
108 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
107 (txt' |
109 (txt' |
108 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |
110 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |