src/Pure/Isar/outer_syntax.ML
changeset 44478 4fdb1009a370
parent 44357 5f5649ac8235
child 44658 5bec9c15ef29
equal deleted inserted replaced
44477:086bb1083552 44478:4fdb1009a370
    32   val scan: Position.T -> string -> Token.T list
    32   val scan: Position.T -> string -> Token.T list
    33   val parse: Position.T -> string -> Toplevel.transition list
    33   val parse: Position.T -> string -> Toplevel.transition list
    34   val process_file: Path.T -> theory -> theory
    34   val process_file: Path.T -> theory -> theory
    35   type isar
    35   type isar
    36   val isar: TextIO.instream -> bool -> isar
    36   val isar: TextIO.instream -> bool -> isar
    37   val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
    37   val read_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
    38   val prepare_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
    38   val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
    39     (Toplevel.transition * Toplevel.transition list) list
    39     (Toplevel.transition * Toplevel.transition list) list
    40   val prepare_command: Position.T -> string -> Toplevel.transition
    40   val read_command: Position.T -> string -> Toplevel.transition
    41 end;
    41 end;
    42 
    42 
    43 structure Outer_Syntax: OUTER_SYNTAX =
    43 structure Outer_Syntax: OUTER_SYNTAX =
    44 struct
    44 struct
    45 
    45 
   249   |> Symbol.source
   249   |> Symbol.source
   250   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   250   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   251   |> toplevel_source term (SOME true) lookup_commands_dynamic;
   251   |> toplevel_source term (SOME true) lookup_commands_dynamic;
   252 
   252 
   253 
   253 
   254 (* prepare toplevel commands -- fail-safe *)
   254 (* read toplevel commands -- fail-safe *)
   255 
   255 
   256 val not_singleton = "Exactly one command expected";
   256 val not_singleton = "Exactly one command expected";
   257 
   257 
   258 fun prepare_span outer_syntax span =
   258 fun read_span outer_syntax span =
   259   let
   259   let
   260     val commands = lookup_commands outer_syntax;
   260     val commands = lookup_commands outer_syntax;
   261     val range_pos = Position.set_range (Thy_Syntax.span_range span);
   261     val range_pos = Position.set_range (Thy_Syntax.span_range span);
   262     val toks = Thy_Syntax.span_content span;
   262     val toks = Thy_Syntax.span_content span;
   263     val _ = List.app Thy_Syntax.report_token toks;
   263     val _ = List.app Thy_Syntax.report_token toks;
   270     | [] => (Toplevel.ignored range_pos, false)
   270     | [] => (Toplevel.ignored range_pos, false)
   271     | _ => (Toplevel.malformed range_pos not_singleton, true))
   271     | _ => (Toplevel.malformed range_pos not_singleton, true))
   272     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   272     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   273   end;
   273   end;
   274 
   274 
   275 fun prepare_element outer_syntax init {head, proof, proper_proof} =
   275 fun read_element outer_syntax init {head, proof, proper_proof} =
   276   let
   276   let
   277     val (tr, proper_head) = prepare_span outer_syntax head |>> Toplevel.modify_init init;
   277     val (tr, proper_head) = read_span outer_syntax head |>> Toplevel.modify_init init;
   278     val proof_trs = map (prepare_span outer_syntax) proof |> filter #2 |> map #1;
   278     val proof_trs = map (read_span outer_syntax) proof |> filter #2 |> map #1;
   279   in
   279   in
   280     if proper_head andalso proper_proof then [(tr, proof_trs)]
   280     if proper_head andalso proper_proof then [(tr, proof_trs)]
   281     else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
   281     else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
   282   end;
   282   end;
   283 
   283 
   284 fun prepare_command pos str =
   284 fun read_command pos str =
   285   let val (lexs, outer_syntax) = get_syntax () in
   285   let val (lexs, outer_syntax) = get_syntax () in
   286     (case Thy_Syntax.parse_spans lexs pos str of
   286     (case Thy_Syntax.parse_spans lexs pos str of
   287       [span] => #1 (prepare_span outer_syntax span)
   287       [span] => #1 (read_span outer_syntax span)
   288     | _ => Toplevel.malformed pos not_singleton)
   288     | _ => Toplevel.malformed pos not_singleton)
   289   end;
   289   end;
   290 
   290 
   291 end;
   291 end;
   292 
   292