equal
deleted
inserted
replaced
43 { |
43 { |
44 /* diagnostics */ |
44 /* diagnostics */ |
45 |
45 |
46 def diagnostics: List[Text.Info[Command.Results]] = |
46 def diagnostics: List[Text.Info[Command.Results]] = |
47 snapshot.cumulate[Command.Results]( |
47 snapshot.cumulate[Command.Results]( |
48 Text.Range.full, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ => |
48 model.doc.full_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ => |
49 { |
49 { |
50 case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body))) |
50 case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body))) |
51 if body.nonEmpty => Some(res + (i -> msg)) |
51 if body.nonEmpty => Some(res + (i -> msg)) |
52 |
52 |
53 case _ => None |
53 case _ => None |