# HG changeset patch
# User wenzelm
# Date 1300737404 -3600
# Node ID 2055515c9d3f842166b8fdc3c3ef357be56e4deb
# Parent  264f8d0e899ff73281071d6b1cad52c9bafa018c
clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;

diff -r 264f8d0e899f -r 2055515c9d3f src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Mon Mar 21 20:15:03 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Mon Mar 21 20:56:44 2011 +0100
@@ -55,11 +55,10 @@
   val prop_tr': term -> term
   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
-  val pts_to_asts: Proof.context ->
-    (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) ->
-    Parser.parsetree list -> Ast.ast list
-  val asts_to_terms: Proof.context ->
-    (string -> (Proof.context -> term list -> term) option) -> Ast.ast list -> term list
+  val parsetree_to_ast: Proof.context ->
+    (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
+  val ast_to_term: Proof.context ->
+    (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
 end;
 
 structure Syn_Trans: SYN_TRANS =
@@ -534,29 +533,24 @@
 
 
 
-(** pts_to_asts **)
+(** parsetree_to_ast **)
 
-fun pts_to_asts ctxt trf pts =
+fun parsetree_to_ast ctxt trf =
   let
     fun trans a args =
       (case trf a of
         NONE => Ast.mk_appl (Ast.Constant a) args
       | SOME f => f ctxt args);
 
-    (*translate pt bottom-up*)
     fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
       | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
-
-    val exn_results = map (Exn.interruptible_capture ast_of) pts;
-    val exns = map_filter Exn.get_exn exn_results;
-    val results = map_filter Exn.get_result exn_results
-  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
+  in ast_of end;
 
 
 
-(** asts_to_terms **)
+(** ast_to_term **)
 
-fun asts_to_terms ctxt trf asts =
+fun ast_to_term ctxt trf =
   let
     fun trans a args =
       (case trf a of
@@ -570,10 +564,6 @@
       | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
           Term.list_comb (term_of ast, map term_of asts)
       | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
-
-    val exn_results = map (Exn.interruptible_capture term_of) asts;
-    val exns = map_filter Exn.get_exn exn_results;
-    val results = map_filter Exn.get_result exn_results
-  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
+  in term_of end;
 
 end;
diff -r 264f8d0e899f -r 2055515c9d3f src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Mar 21 20:15:03 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Mar 21 20:56:44 2011 +0100
@@ -714,18 +714,22 @@
 
     val limit = Config.get ctxt ambiguity_limit;
     fun show_pt pt =
-      Pretty.string_of (Ast.pretty_ast (hd (Syn_Trans.pts_to_asts ctxt (K NONE) [pt])));
-  in
-    if len <= Config.get ctxt ambiguity_level then ()
-    else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
-    else
-      (Context_Position.if_visible ctxt warning (cat_lines
-        (("Ambiguous input" ^ Position.str_of pos ^
-          "\nproduces " ^ string_of_int len ^ " parse trees" ^
-          (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-          map show_pt (take limit pts))));
-    Syn_Trans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
-  end;
+      Pretty.string_of (Ast.pretty_ast (Syn_Trans.parsetree_to_ast ctxt (K NONE) pt));
+    val _ =
+      if len <= Config.get ctxt ambiguity_level then ()
+      else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
+      else
+        (Context_Position.if_visible ctxt warning (cat_lines
+          (("Ambiguous input" ^ Position.str_of pos ^
+            "\nproduces " ^ string_of_int len ^ " parse trees" ^
+            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
+            map show_pt (take limit pts))));
+
+    val ast_of = Syn_Trans.parsetree_to_ast ctxt (lookup_tr parse_ast_trtab);
+    val exn_results = map (Exn.interruptible_capture ast_of) pts;
+    val exns = map_filter Exn.get_exn exn_results;
+    val results = map_filter Exn.get_result exn_results
+  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
 
 
 (* read *)
@@ -733,11 +737,14 @@
 fun read ctxt (syn as Syntax (tabs, _)) root inp =
   let
     val {parse_ruletab, parse_trtab, ...} = tabs;
-    val asts = read_asts ctxt syn false root inp;
-  in
-    Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
-      (map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)) asts)
-  end;
+    val asts = read_asts ctxt syn false root inp
+      |> map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab));
+
+    val term_of = Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab);
+    val exn_results = map (Exn.interruptible_capture term_of) asts;
+    val exns = map_filter Exn.get_exn exn_results;
+    val results = map_filter Exn.get_result exn_results
+  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
 
 
 (* read terms *)