src/Pure/Isar/outer_syntax.ML

     (local_theory -> Proof.state) parser -> unit
   val bootstrap: bool Config.T
   val parse_tokens: theory -> Token.T list -> Toplevel.transition list
   val parse: theory -> Position.T -> string -> Toplevel.transition list
   val parse_spans: Token.T list -> Command_Span.span list
+  val make_span: Token.T list -> Command_Span.span
   val command_reports: theory -> Token.T -> Position.report_text list
   val check_command: Proof.context -> command_keyword -> string
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =

 fun parse_spans toks =
   fold parse toks ([], [], []) |> flush |> rev;
 
 end;
 
+fun make_span toks =
+  (case parse_spans toks of
+    [span] => span
+  | _ => Command_Span.Span (Command_Span.Malformed_Span, toks));
+
 
 (* check commands *)
 
 fun command_reports thy tok =
   if Token.is_command tok then