equal
deleted
inserted
replaced
78 let |
78 let |
79 val txt = |
79 val txt = |
80 if txt2 = "" then txt1 |
80 if txt2 = "" then txt1 |
81 else if kind = "type" then txt1 ^ " = " ^ txt2 |
81 else if kind = "type" then txt1 ^ " = " ^ txt2 |
82 else if kind = "exception" then txt1 ^ " of " ^ txt2 |
82 else if kind = "exception" then txt1 ^ " of " ^ txt2 |
83 else if Lexicon.is_identifier (Long_Name.base_name (ml_name txt1)) |
83 else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1)) |
84 then txt1 ^ ": " ^ txt2 |
84 then txt1 ^ ": " ^ txt2 |
85 else txt1 ^ " : " ^ txt2; |
85 else txt1 ^ " : " ^ txt2; |
86 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
86 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
87 val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2)); (* ML_Lex.read (!?) *) |
87 val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2)); (* ML_Lex.read (!?) *) |
88 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
88 val kind' = if kind = "" then "ML" else "ML " ^ kind; |