equal
deleted
inserted
replaced
97 |
97 |
98 fun print_entry_ref kind (name, entry) = |
98 fun print_entry_ref kind (name, entry) = |
99 quote (Markup.markup (entry_markup false kind (name, entry)) name); |
99 quote (Markup.markup (entry_markup false kind (name, entry)) name); |
100 |
100 |
101 fun err_dup kind entry1 entry2 pos = |
101 fun err_dup kind entry1 entry2 pos = |
102 error ("Duplicate " ^ kind ^ " declaration " ^ |
102 error ("Duplicate " ^ plain_words kind ^ " declaration " ^ |
103 print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos); |
103 print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos); |
104 |
104 |
105 fun undefined kind name = "Undefined " ^ kind ^ ": " ^ quote name; |
105 fun undefined kind name = "Undefined " ^ plain_words kind ^ ": " ^ quote name; |
106 |
106 |
107 |
107 |
108 (* datatype T *) |
108 (* datatype T *) |
109 |
109 |
110 datatype T = |
110 datatype T = |