44package de .uka .ilkd .key .nparser .builder ;
55
66import java .util .*;
7+ import java .util .stream .Collectors ;
8+ import java .util .stream .Stream ;
79
810import de .uka .ilkd .key .java .Services ;
911import de .uka .ilkd .key .java .abstraction .KeYJavaType ;
@@ -68,8 +70,9 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) {
6870 var origin = BuilderHelpers .getPosition (ctx );
6971 List <GenericParameter > typeParameters = accept (ctx .formal_sort_param_decls ());
7072 if (typeParameters == null ) {
71- var s = new SortImpl (new Name (name ), ImmutableSet .empty (), false , doc , origin );
73+ var s = new SortImpl (new Name (name ), ImmutableSet .empty (), false , origin );
7274 sorts ().addSafely (s );
75+ docsSpace ().describe (s , doc );
7376 } else {
7477 var doubled = CollectionUtil .findDuplicates (typeParameters );
7578 if (!doubled .isEmpty ()) {
@@ -78,10 +81,10 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) {
7881 doubled .getFirst ());
7982 }
8083 var s = new ParametricSortDecl (new Name (name ), false , ImmutableSet .empty (),
81- ImmutableList .fromList (typeParameters ), doc , origin );
84+ ImmutableList .fromList (typeParameters ), origin );
8285 namespaces ().parametricSorts ().addSafely (s );
86+ docsSpace ().describe (s , doc );
8387 }
84- docsSpace ().describe (s , doc );
8588 return null ;
8689 }
8790
@@ -257,8 +260,13 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) {
257260 sortName );
258261 }
259262 var sortDecl = new ParametricSortDecl (sortName , isAbstractSort , ext , params ,
260- documentation , BuilderHelpers .getPosition (declCtx ));
263+ BuilderHelpers .getPosition (declCtx ));
261264 namespaces ().parametricSorts ().addSafely (sortDecl );
265+
266+ var doc = processDocumentation (declCtx .DOC_COMMENT ());
267+ docsSpace ().describe (sortDecl ,
268+ Stream .of (doc , sectionDoc ).filter (Objects ::nonNull )
269+ .collect (Collectors .joining ("\n " )));
262270 }
263271 return createdSorts ;
264272 }
0 commit comments