src/Pure/Isar/outer_syntax.ML
changeset 51268 fcc4b89a600d
parent 51225 3fe0d8d55975
child 51271 e8d2ecf6aaac
equal deleted inserted replaced
51267:c68c1b89a0f1 51268:fcc4b89a600d
    33   val scan: Position.T -> string -> Token.T list
    33   val scan: Position.T -> string -> Token.T list
    34   val parse: Position.T -> string -> Toplevel.transition list
    34   val parse: Position.T -> string -> Toplevel.transition list
    35   type isar
    35   type isar
    36   val isar: TextIO.instream -> bool -> isar
    36   val isar: TextIO.instream -> bool -> isar
    37   val span_cmts: Token.T list -> Token.T list
    37   val span_cmts: Token.T list -> Token.T list
    38   val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
    38   val read_span: outer_syntax -> Token.T list -> Toplevel.transition
    39   val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.span Thy_Syntax.element ->
       
    40     (Toplevel.transition * Toplevel.transition list) list
       
    41 end;
    39 end;
    42 
    40 
    43 structure Outer_Syntax: OUTER_SYNTAX =
    41 structure Outer_Syntax: OUTER_SYNTAX =
    44 struct
    42 struct
    45 
    43 
   317       else [];
   315       else [];
   318 
   316 
   319     val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
   317     val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
   320     val _ = Position.reports_text (token_reports @ maps command_reports toks);
   318     val _ = Position.reports_text (token_reports @ maps command_reports toks);
   321   in
   319   in
   322     if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true)
   320     if is_malformed then Toplevel.malformed pos "Malformed command syntax"
   323     else
   321     else
   324       (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
   322       (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
   325         [tr] =>
   323         [tr] =>
   326           if Keyword.is_control (Toplevel.name_of tr) then
   324           if Keyword.is_control (Toplevel.name_of tr) then
   327             (Toplevel.malformed pos "Illegal control command", true)
   325             Toplevel.malformed pos "Illegal control command"
   328           else (tr, true)
   326           else tr
   329       | [] => (Toplevel.ignored (Position.set_range (Command.range toks)), false)
   327       | [] => Toplevel.ignored (Position.set_range (Command.range toks))
   330       | _ => (Toplevel.malformed proper_range "Exactly one command expected", true))
   328       | _ => Toplevel.malformed proper_range "Exactly one command expected")
   331       handle ERROR msg => (Toplevel.malformed proper_range msg, true)
   329       handle ERROR msg => Toplevel.malformed proper_range msg
   332   end;
   330   end;
   333 
   331 
   334 fun read_element outer_syntax init (Thy_Syntax.Element (head, opt_proof)) =
   332 end;
   335   let
   333 
   336     val read = read_span outer_syntax o Thy_Syntax.span_content;
       
   337     val (tr, proper_head) = read head |>> Toplevel.modify_init init;
       
   338     val proof_trs =
       
   339       (case opt_proof of
       
   340         NONE => []
       
   341       | SOME (a, b) => map read (maps Thy_Syntax.flat_element a @ [b]) |> filter #2 |> map #1);
       
   342   in
       
   343     if proper_head andalso
       
   344       not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
       
   345     else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
       
   346   end;
       
   347 
       
   348 end;
       
   349