From e8b4756c655eacd8a2b9b23630ba02dbbbc4e96e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Mar 2015 18:17:03 +0100
Subject: Putting the From parameter of the Require command into the AST.

---
 stm/texmacspp.ml | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

(limited to 'stm')

diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index a0979f8b15..083fd54bfa 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -617,14 +617,17 @@ let rec tmpp v loc =
   | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
   | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
   | VernacNameSectionHypSet _ as x -> xmlTODO loc x
-  | VernacRequire (None,l) ->
-      xmlRequire loc (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacRequire (Some true,l) ->
-      xmlRequire loc ~attr:["export","true"] (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacRequire (Some false,l) ->
-      xmlRequire loc ~attr:["import","true"] (List.map (fun ref ->
+  | VernacRequire (from, import, l) ->
+      let import = match import with
+      | None -> []
+      | Some true -> ["export","true"]
+      | Some false -> ["import","true"]
+      in
+      let from = match from with
+      | None -> []
+      | Some r -> ["from", Libnames.string_of_reference r]
+      in
+      xmlRequire loc ~attr:(from @ import) (List.map (fun ref ->
         xmlReference ref) l)
   | VernacImport (true,l) ->
       xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
-- 
cgit v1.2.3