src/Pure/Isar/outer_syntax.ML
changeset 68184 6c693b2700b3
parent 67499 bbb86f719d4b
child 68729 3a02b424d5fb
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon May 14 22:01:00 2018 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon May 14 22:22:47 2018 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4    val parse_tokens: theory -> Token.T list -> Toplevel.transition list
     1.5    val parse: theory -> Position.T -> string -> Toplevel.transition list
     1.6    val parse_spans: Token.T list -> Command_Span.span list
     1.7 +  val make_span: Token.T list -> Command_Span.span
     1.8    val command_reports: theory -> Token.T -> Position.report_text list
     1.9    val check_command: Proof.context -> command_keyword -> string
    1.10  end;
    1.11 @@ -260,6 +261,11 @@
    1.12  
    1.13  end;
    1.14  
    1.15 +fun make_span toks =
    1.16 +  (case parse_spans toks of
    1.17 +    [span] => span
    1.18 +  | _ => Command_Span.Span (Command_Span.Malformed_Span, toks));
    1.19 +
    1.20  
    1.21  (* check commands *)
    1.22