equal
deleted
inserted
replaced
118 val thy_heading = "\nTheory " + quote(thy) + ":" |
118 val thy_heading = "\nTheory " + quote(thy) + ":" |
119 read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols) |
119 read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols) |
120 match { |
120 match { |
121 case None => progress.echo(thy_heading + " MISSING") |
121 case None => progress.echo(thy_heading + " MISSING") |
122 case Some(command) => |
122 case Some(command) => |
123 val snapshot = Document.State.init.command_snippet(command) |
123 val snapshot = Document.State.init.snippet(command) |
124 val rendering = new Rendering(snapshot, options, session) |
124 val rendering = new Rendering(snapshot, options, session) |
125 val messages = |
125 val messages = |
126 rendering.text_messages(Text.Range.full) |
126 rendering.text_messages(Text.Range.full) |
127 .filter(message => verbose || Protocol.is_exported(message.info)) |
127 .filter(message => verbose || Protocol.is_exported(message.info)) |
128 if (messages.nonEmpty) { |
128 if (messages.nonEmpty) { |